%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM436+3 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n001.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:45 EDT 2023 % Result : Theorem 11.76s 2.34s % Output : Proof 17.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM436+3 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.33 % Computer : n001.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 09:14:58 EDT 2023 % 0.20/0.34 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.60 ___ __ \_________(_)________________________________ % 0.20/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.60 (2023-06-19) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2023 % 0.20/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.60 Amanda Stjerna. % 0.20/0.60 Free software under BSD-3-Clause. % 0.20/0.60 % 0.20/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.60 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 0.20/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.82/1.11 Prover 1: Preprocessing ... % 2.82/1.11 Prover 4: Preprocessing ... % 3.12/1.15 Prover 5: Preprocessing ... % 3.12/1.15 Prover 2: Preprocessing ... % 3.12/1.15 Prover 3: Preprocessing ... % 3.12/1.15 Prover 0: Preprocessing ... % 3.12/1.15 Prover 6: Preprocessing ... % 6.33/1.63 Prover 1: Constructing countermodel ... % 6.33/1.66 Prover 3: Constructing countermodel ... % 6.91/1.67 Prover 6: Proving ... % 7.39/1.76 Prover 5: Constructing countermodel ... % 8.08/1.84 Prover 2: Proving ... % 8.08/1.85 Prover 4: Constructing countermodel ... % 8.58/1.89 Prover 0: Proving ... % 11.76/2.34 Prover 3: proved (1719ms) % 11.76/2.34 % 11.76/2.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.76/2.34 % 11.76/2.34 Prover 5: stopped % 11.76/2.34 Prover 6: stopped % 11.86/2.36 Prover 0: stopped % 11.86/2.36 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.86/2.36 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.86/2.36 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 11.86/2.36 Prover 2: stopped % 11.86/2.36 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 11.86/2.36 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.30/2.42 Prover 8: Preprocessing ... % 12.30/2.43 Prover 10: Preprocessing ... % 12.30/2.43 Prover 7: Preprocessing ... % 12.30/2.43 Prover 11: Preprocessing ... % 12.30/2.45 Prover 13: Preprocessing ... % 12.58/2.53 Prover 8: Warning: ignoring some quantifiers % 12.58/2.53 Prover 8: Constructing countermodel ... % 13.21/2.56 Prover 7: Constructing countermodel ... % 13.21/2.57 Prover 10: Constructing countermodel ... % 13.52/2.62 Prover 13: Constructing countermodel ... % 13.99/2.64 Prover 11: Constructing countermodel ... % 15.37/2.94 Prover 1: Found proof (size 335) % 15.37/2.94 Prover 1: proved (2321ms) % 15.37/2.94 Prover 4: stopped % 15.37/2.94 Prover 10: stopped % 15.37/2.94 Prover 11: stopped % 15.37/2.94 Prover 8: stopped % 15.37/2.94 Prover 13: stopped % 15.37/2.94 Prover 7: stopped % 15.37/2.94 % 15.37/2.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.37/2.94 % 16.44/3.02 % SZS output start Proof for theBenchmark % 16.44/3.02 Assumptions after simplification: % 16.44/3.02 --------------------------------- % 16.44/3.02 % 16.44/3.02 (mDivisor) % 16.51/3.05 $i(sz00) & ! [v0: $i] : ( ~ (aInteger0(v0) = 0) | ~ $i(v0) | ( ! [v1: $i] : % 16.51/3.05 ! [v2: int] : (v2 = 0 | v1 = sz00 | ~ (aDivisorOf0(v1, v0) = v2) | ~ % 16.51/3.05 $i(v1) | ? [v3: int] : ( ~ (v3 = 0) & aInteger0(v1) = v3) | ! [v3: $i] % 16.51/3.05 : ( ~ (sdtasdt0(v1, v3) = v0) | ~ $i(v3) | ? [v4: int] : ( ~ (v4 = 0) % 16.51/3.05 & aInteger0(v3) = v4))) & ! [v1: $i] : ( ~ (aDivisorOf0(v1, v0) = % 16.51/3.05 0) | ~ $i(v1) | ( ~ (v1 = sz00) & aInteger0(v1) = 0 & ? [v2: $i] : % 16.51/3.05 (sdtasdt0(v1, v2) = v0 & aInteger0(v2) = 0 & $i(v2)))))) % 16.51/3.05 % 16.51/3.05 (mIntMult) % 16.51/3.05 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 16.51/3.05 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 16.51/3.05 (aInteger0(v2) = v5 & aInteger0(v1) = v4 & aInteger0(v0) = v3 & ( ~ (v4 = 0) % 16.51/3.05 | ~ (v3 = 0) | v5 = 0))) % 16.51/3.05 % 16.51/3.05 (mIntPlus) % 16.51/3.05 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ % 16.51/3.05 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 16.51/3.05 (aInteger0(v2) = v5 & aInteger0(v1) = v4 & aInteger0(v0) = v3 & ( ~ (v4 = 0) % 16.51/3.05 | ~ (v3 = 0) | v5 = 0))) % 16.51/3.05 % 16.51/3.05 (mMulAsso) % 16.51/3.06 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 16.51/3.06 (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 16.51/3.06 | ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? % 16.51/3.06 [v9: $i] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & aInteger0(v2) = % 16.51/3.06 v7 & aInteger0(v1) = v6 & aInteger0(v0) = v5 & $i(v9) & $i(v8) & ( ~ (v7 = % 16.51/3.06 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 16.51/3.06 % 16.51/3.06 (mMulComm) % 16.51/3.06 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ % 16.51/3.06 $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: $i] : % 16.51/3.06 (sdtasdt0(v1, v0) = v5 & aInteger0(v1) = v4 & aInteger0(v0) = v3 & $i(v5) & % 16.51/3.06 ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 16.51/3.06 % 16.51/3.06 (m__) % 16.51/3.06 $i(xq) & $i(xp) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? [v2: any] : % 16.51/3.06 ? [v3: any] : ? [v4: any] : ? [v5: any] : (sdteqdtlpzmzozddtrp0(xa, xb, xq) % 16.51/3.06 = v5 & sdteqdtlpzmzozddtrp0(xa, xb, xp) = v3 & aDivisorOf0(xq, v1) = v4 & % 16.51/3.06 aDivisorOf0(xp, v1) = v2 & sdtpldt0(xa, v0) = v1 & smndt0(xb) = v0 & $i(v1) % 16.51/3.06 & $i(v0) & (( ~ (v5 = 0) & ~ (v4 = 0) & ! [v6: $i] : ( ~ (sdtasdt0(xq, v6) % 16.51/3.06 = v1) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = 0) & aInteger0(v6) = % 16.51/3.06 v7))) | ( ~ (v3 = 0) & ~ (v2 = 0) & ! [v6: $i] : ( ~ (sdtasdt0(xp, % 16.51/3.06 v6) = v1) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = 0) & % 16.51/3.06 aInteger0(v6) = v7))))) % 16.51/3.06 % 16.51/3.06 (m__1003) % 16.51/3.06 $i(xq) & $i(xp) & $i(xb) & $i(xa) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? % 16.51/3.06 [v2: $i] : ( ~ (v0 = sz00) & sdteqdtlpzmzozddtrp0(xa, xb, v0) = 0 & % 16.51/3.06 aDivisorOf0(v0, v2) = 0 & sdtasdt0(xp, xq) = v0 & sdtpldt0(xa, v1) = v2 & % 16.51/3.06 smndt0(xb) = v1 & $i(v2) & $i(v1) & $i(v0) & ? [v3: $i] : (sdtasdt0(v0, v3) % 16.51/3.06 = v2 & aInteger0(v3) = 0 & $i(v3))) % 16.51/3.06 % 16.51/3.06 (m__1032) % 16.51/3.06 $i(xm) & $i(xq) & $i(xp) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? % 16.51/3.06 [v2: $i] : (sdtasdt0(v0, xm) = v1 & sdtasdt0(xp, xq) = v0 & sdtpldt0(xa, v2) = % 16.51/3.06 v1 & smndt0(xb) = v2 & aInteger0(xm) = 0 & $i(v2) & $i(v1) & $i(v0)) % 16.51/3.06 % 16.51/3.06 (m__1071) % 16.51/3.07 $i(xm) & $i(xq) & $i(xp) & $i(xb) & $i(xa) & ? [v0: $i] : ? [v1: $i] : ? % 16.51/3.07 [v2: $i] : ? [v3: $i] : (sdtasdt0(xq, v3) = v1 & sdtasdt0(xq, xm) = v0 & % 16.51/3.07 sdtasdt0(xp, v0) = v1 & sdtasdt0(xp, xm) = v3 & sdtpldt0(xa, v2) = v1 & % 16.51/3.07 smndt0(xb) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 16.51/3.07 % 16.51/3.07 (m__979) % 16.51/3.07 ~ (xq = sz00) & ~ (xp = sz00) & aInteger0(xq) = 0 & aInteger0(xp) = 0 & % 16.51/3.07 aInteger0(xb) = 0 & aInteger0(xa) = 0 & $i(xq) & $i(xp) & $i(xb) & $i(xa) & % 16.51/3.07 $i(sz00) % 16.51/3.07 % 16.51/3.07 (function-axioms) % 16.51/3.07 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 16.51/3.07 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) % 16.51/3.07 | ~ (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 16.51/3.07 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 16.51/3.07 (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & ! [v0: $i] : % 16.51/3.07 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) % 16.51/3.07 | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 16.51/3.07 [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 16.51/3.07 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = v1) | % 16.51/3.07 ~ (smndt0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 16.51/3.07 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (aInteger0(v2) = v1) | ~ % 16.51/3.07 (aInteger0(v2) = v0)) % 16.51/3.07 % 16.51/3.07 Further assumptions not needed in the proof: % 16.51/3.07 -------------------------------------------- % 16.51/3.07 mAddAsso, mAddComm, mAddNeg, mAddZero, mDistrib, mEquMod, mEquModRef, % 16.51/3.07 mEquModSym, mEquModTrn, mIntNeg, mIntOne, mIntZero, mIntegers, mMulMinOne, % 16.51/3.07 mMulOne, mMulZero, mZeroDiv % 16.51/3.07 % 16.51/3.07 Those formulas are unsatisfiable: % 16.51/3.07 --------------------------------- % 16.51/3.07 % 16.51/3.07 Begin of proof % 16.51/3.07 | % 16.51/3.07 | ALPHA: (mDivisor) implies: % 16.51/3.08 | (1) ! [v0: $i] : ( ~ (aInteger0(v0) = 0) | ~ $i(v0) | ( ! [v1: $i] : ! % 16.51/3.08 | [v2: int] : (v2 = 0 | v1 = sz00 | ~ (aDivisorOf0(v1, v0) = v2) | % 16.51/3.08 | ~ $i(v1) | ? [v3: int] : ( ~ (v3 = 0) & aInteger0(v1) = v3) | ! % 16.51/3.08 | [v3: $i] : ( ~ (sdtasdt0(v1, v3) = v0) | ~ $i(v3) | ? [v4: int] % 16.51/3.08 | : ( ~ (v4 = 0) & aInteger0(v3) = v4))) & ! [v1: $i] : ( ~ % 16.51/3.08 | (aDivisorOf0(v1, v0) = 0) | ~ $i(v1) | ( ~ (v1 = sz00) & % 16.51/3.08 | aInteger0(v1) = 0 & ? [v2: $i] : (sdtasdt0(v1, v2) = v0 & % 16.51/3.08 | aInteger0(v2) = 0 & $i(v2)))))) % 16.51/3.08 | % 16.51/3.08 | ALPHA: (m__979) implies: % 16.51/3.08 | (2) ~ (xp = sz00) % 16.51/3.08 | (3) ~ (xq = sz00) % 16.51/3.08 | (4) aInteger0(xp) = 0 % 16.51/3.08 | (5) aInteger0(xq) = 0 % 16.51/3.08 | % 16.51/3.08 | ALPHA: (m__1003) implies: % 16.51/3.08 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v0 = sz00) & % 16.51/3.08 | sdteqdtlpzmzozddtrp0(xa, xb, v0) = 0 & aDivisorOf0(v0, v2) = 0 & % 16.51/3.08 | sdtasdt0(xp, xq) = v0 & sdtpldt0(xa, v1) = v2 & smndt0(xb) = v1 & % 16.51/3.08 | $i(v2) & $i(v1) & $i(v0) & ? [v3: $i] : (sdtasdt0(v0, v3) = v2 & % 16.51/3.08 | aInteger0(v3) = 0 & $i(v3))) % 16.51/3.08 | % 16.51/3.08 | ALPHA: (m__1032) implies: % 16.51/3.08 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (sdtasdt0(v0, xm) = v1 & % 16.51/3.08 | sdtasdt0(xp, xq) = v0 & sdtpldt0(xa, v2) = v1 & smndt0(xb) = v2 & % 16.51/3.08 | aInteger0(xm) = 0 & $i(v2) & $i(v1) & $i(v0)) % 16.51/3.08 | % 16.51/3.08 | ALPHA: (m__1071) implies: % 16.51/3.08 | (8) $i(xm) % 16.51/3.08 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (sdtasdt0(xq, % 16.51/3.08 | v3) = v1 & sdtasdt0(xq, xm) = v0 & sdtasdt0(xp, v0) = v1 & % 16.51/3.08 | sdtasdt0(xp, xm) = v3 & sdtpldt0(xa, v2) = v1 & smndt0(xb) = v2 & % 16.51/3.08 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 16.51/3.08 | % 16.51/3.08 | ALPHA: (m__) implies: % 16.51/3.08 | (10) $i(xa) % 16.51/3.08 | (11) $i(xp) % 16.51/3.08 | (12) $i(xq) % 16.51/3.08 | (13) ? [v0: $i] : ? [v1: $i] : ? [v2: any] : ? [v3: any] : ? [v4: any] % 16.51/3.08 | : ? [v5: any] : (sdteqdtlpzmzozddtrp0(xa, xb, xq) = v5 & % 16.51/3.08 | sdteqdtlpzmzozddtrp0(xa, xb, xp) = v3 & aDivisorOf0(xq, v1) = v4 & % 16.51/3.08 | aDivisorOf0(xp, v1) = v2 & sdtpldt0(xa, v0) = v1 & smndt0(xb) = v0 & % 16.51/3.08 | $i(v1) & $i(v0) & (( ~ (v5 = 0) & ~ (v4 = 0) & ! [v6: $i] : ( ~ % 16.51/3.08 | (sdtasdt0(xq, v6) = v1) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = % 16.51/3.08 | 0) & aInteger0(v6) = v7))) | ( ~ (v3 = 0) & ~ (v2 = 0) & % 16.51/3.08 | ! [v6: $i] : ( ~ (sdtasdt0(xp, v6) = v1) | ~ $i(v6) | ? [v7: % 16.51/3.08 | int] : ( ~ (v7 = 0) & aInteger0(v6) = v7))))) % 16.51/3.08 | % 16.51/3.08 | ALPHA: (function-axioms) implies: % 16.51/3.08 | (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 16.51/3.08 | : (v1 = v0 | ~ (aInteger0(v2) = v1) | ~ (aInteger0(v2) = v0)) % 16.51/3.08 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (smndt0(v2) = % 16.51/3.08 | v1) | ~ (smndt0(v2) = v0)) % 16.51/3.09 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 16.51/3.09 | (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 16.51/3.09 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 16.51/3.09 | (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 16.51/3.09 | % 16.51/3.09 | DELTA: instantiating (7) with fresh symbols all_22_0, all_22_1, all_22_2 % 16.51/3.09 | gives: % 16.51/3.09 | (18) sdtasdt0(all_22_2, xm) = all_22_1 & sdtasdt0(xp, xq) = all_22_2 & % 16.51/3.09 | sdtpldt0(xa, all_22_0) = all_22_1 & smndt0(xb) = all_22_0 & % 16.51/3.09 | aInteger0(xm) = 0 & $i(all_22_0) & $i(all_22_1) & $i(all_22_2) % 16.51/3.09 | % 16.51/3.09 | ALPHA: (18) implies: % 16.51/3.09 | (19) aInteger0(xm) = 0 % 16.51/3.09 | (20) smndt0(xb) = all_22_0 % 16.51/3.09 | (21) sdtpldt0(xa, all_22_0) = all_22_1 % 16.51/3.09 | (22) sdtasdt0(xp, xq) = all_22_2 % 16.51/3.09 | (23) sdtasdt0(all_22_2, xm) = all_22_1 % 16.51/3.09 | % 16.51/3.09 | DELTA: instantiating (9) with fresh symbols all_24_0, all_24_1, all_24_2, % 16.51/3.09 | all_24_3 gives: % 16.51/3.09 | (24) sdtasdt0(xq, all_24_0) = all_24_2 & sdtasdt0(xq, xm) = all_24_3 & % 16.51/3.09 | sdtasdt0(xp, all_24_3) = all_24_2 & sdtasdt0(xp, xm) = all_24_0 & % 16.51/3.09 | sdtpldt0(xa, all_24_1) = all_24_2 & smndt0(xb) = all_24_1 & % 16.51/3.09 | $i(all_24_0) & $i(all_24_1) & $i(all_24_2) & $i(all_24_3) % 16.51/3.09 | % 16.51/3.09 | ALPHA: (24) implies: % 16.51/3.09 | (25) $i(all_24_3) % 16.51/3.09 | (26) $i(all_24_1) % 16.51/3.09 | (27) $i(all_24_0) % 16.51/3.09 | (28) smndt0(xb) = all_24_1 % 16.51/3.09 | (29) sdtpldt0(xa, all_24_1) = all_24_2 % 16.51/3.09 | (30) sdtasdt0(xp, xm) = all_24_0 % 16.51/3.09 | (31) sdtasdt0(xp, all_24_3) = all_24_2 % 16.51/3.09 | (32) sdtasdt0(xq, xm) = all_24_3 % 16.51/3.09 | (33) sdtasdt0(xq, all_24_0) = all_24_2 % 16.51/3.09 | % 16.51/3.09 | DELTA: instantiating (6) with fresh symbols all_29_0, all_29_1, all_29_2 % 16.51/3.09 | gives: % 16.51/3.09 | (34) ~ (all_29_2 = sz00) & sdteqdtlpzmzozddtrp0(xa, xb, all_29_2) = 0 & % 16.51/3.09 | aDivisorOf0(all_29_2, all_29_0) = 0 & sdtasdt0(xp, xq) = all_29_2 & % 16.51/3.09 | sdtpldt0(xa, all_29_1) = all_29_0 & smndt0(xb) = all_29_1 & % 16.51/3.09 | $i(all_29_0) & $i(all_29_1) & $i(all_29_2) & ? [v0: $i] : % 16.51/3.09 | (sdtasdt0(all_29_2, v0) = all_29_0 & aInteger0(v0) = 0 & $i(v0)) % 16.51/3.09 | % 16.51/3.09 | ALPHA: (34) implies: % 16.51/3.09 | (35) $i(all_29_2) % 16.51/3.09 | (36) smndt0(xb) = all_29_1 % 16.51/3.09 | (37) sdtpldt0(xa, all_29_1) = all_29_0 % 16.51/3.09 | (38) sdtasdt0(xp, xq) = all_29_2 % 16.51/3.09 | (39) ? [v0: $i] : (sdtasdt0(all_29_2, v0) = all_29_0 & aInteger0(v0) = 0 & % 16.51/3.09 | $i(v0)) % 16.51/3.09 | % 16.51/3.09 | DELTA: instantiating (13) with fresh symbols all_31_0, all_31_1, all_31_2, % 16.51/3.09 | all_31_3, all_31_4, all_31_5 gives: % 16.51/3.10 | (40) sdteqdtlpzmzozddtrp0(xa, xb, xq) = all_31_0 & sdteqdtlpzmzozddtrp0(xa, % 16.51/3.10 | xb, xp) = all_31_2 & aDivisorOf0(xq, all_31_4) = all_31_1 & % 16.51/3.10 | aDivisorOf0(xp, all_31_4) = all_31_3 & sdtpldt0(xa, all_31_5) = % 16.51/3.10 | all_31_4 & smndt0(xb) = all_31_5 & $i(all_31_4) & $i(all_31_5) & (( ~ % 16.51/3.10 | (all_31_0 = 0) & ~ (all_31_1 = 0) & ! [v0: $i] : ( ~ % 16.51/3.10 | (sdtasdt0(xq, v0) = all_31_4) | ~ $i(v0) | ? [v1: int] : ( ~ % 16.51/3.10 | (v1 = 0) & aInteger0(v0) = v1))) | ( ~ (all_31_2 = 0) & ~ % 16.51/3.10 | (all_31_3 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = all_31_4) | % 16.51/3.10 | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1)))) % 16.51/3.10 | % 16.51/3.10 | ALPHA: (40) implies: % 16.51/3.10 | (41) smndt0(xb) = all_31_5 % 16.51/3.10 | (42) sdtpldt0(xa, all_31_5) = all_31_4 % 16.51/3.10 | (43) aDivisorOf0(xp, all_31_4) = all_31_3 % 16.51/3.10 | (44) aDivisorOf0(xq, all_31_4) = all_31_1 % 16.51/3.10 | (45) ( ~ (all_31_0 = 0) & ~ (all_31_1 = 0) & ! [v0: $i] : ( ~ % 16.51/3.10 | (sdtasdt0(xq, v0) = all_31_4) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 16.51/3.10 | = 0) & aInteger0(v0) = v1))) | ( ~ (all_31_2 = 0) & ~ % 16.51/3.10 | (all_31_3 = 0) & ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = all_31_4) | % 16.51/3.10 | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1))) % 16.51/3.10 | % 16.51/3.10 | DELTA: instantiating (39) with fresh symbol all_33_0 gives: % 16.51/3.10 | (46) sdtasdt0(all_29_2, all_33_0) = all_29_0 & aInteger0(all_33_0) = 0 & % 16.51/3.10 | $i(all_33_0) % 16.51/3.10 | % 16.51/3.10 | ALPHA: (46) implies: % 16.51/3.10 | (47) $i(all_33_0) % 16.51/3.10 | (48) aInteger0(all_33_0) = 0 % 16.51/3.10 | (49) sdtasdt0(all_29_2, all_33_0) = all_29_0 % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (15) with all_24_1, all_29_1, xb, simplifying with % 16.51/3.10 | (28), (36) gives: % 16.51/3.10 | (50) all_29_1 = all_24_1 % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (15) with all_29_1, all_31_5, xb, simplifying with % 16.51/3.10 | (36), (41) gives: % 16.51/3.10 | (51) all_31_5 = all_29_1 % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (15) with all_22_0, all_31_5, xb, simplifying with % 16.51/3.10 | (20), (41) gives: % 16.51/3.10 | (52) all_31_5 = all_22_0 % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (17) with all_22_2, all_29_2, xq, xp, simplifying % 16.51/3.10 | with (22), (38) gives: % 16.51/3.10 | (53) all_29_2 = all_22_2 % 16.51/3.10 | % 16.51/3.10 | COMBINE_EQS: (51), (52) imply: % 16.51/3.10 | (54) all_29_1 = all_22_0 % 16.51/3.10 | % 16.51/3.10 | SIMP: (54) implies: % 16.51/3.10 | (55) all_29_1 = all_22_0 % 16.51/3.10 | % 16.51/3.10 | COMBINE_EQS: (50), (55) imply: % 16.51/3.10 | (56) all_24_1 = all_22_0 % 16.51/3.10 | % 16.51/3.10 | REDUCE: (49), (53) imply: % 16.51/3.10 | (57) sdtasdt0(all_22_2, all_33_0) = all_29_0 % 16.51/3.10 | % 16.51/3.10 | REDUCE: (42), (52) imply: % 16.51/3.10 | (58) sdtpldt0(xa, all_22_0) = all_31_4 % 16.51/3.10 | % 16.51/3.10 | REDUCE: (37), (55) imply: % 16.51/3.10 | (59) sdtpldt0(xa, all_22_0) = all_29_0 % 16.51/3.10 | % 16.51/3.10 | REDUCE: (29), (56) imply: % 16.51/3.10 | (60) sdtpldt0(xa, all_22_0) = all_24_2 % 16.51/3.10 | % 16.51/3.10 | REDUCE: (35), (53) imply: % 16.51/3.10 | (61) $i(all_22_2) % 16.51/3.10 | % 16.51/3.10 | REDUCE: (26), (56) imply: % 16.51/3.10 | (62) $i(all_22_0) % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (16) with all_22_1, all_29_0, all_22_0, xa, % 16.51/3.10 | simplifying with (21), (59) gives: % 16.51/3.10 | (63) all_29_0 = all_22_1 % 16.51/3.10 | % 16.51/3.10 | GROUND_INST: instantiating (16) with all_29_0, all_31_4, all_22_0, xa, % 16.51/3.10 | simplifying with (58), (59) gives: % 16.51/3.11 | (64) all_31_4 = all_29_0 % 16.51/3.11 | % 16.51/3.11 | GROUND_INST: instantiating (16) with all_24_2, all_31_4, all_22_0, xa, % 16.51/3.11 | simplifying with (58), (60) gives: % 16.51/3.11 | (65) all_31_4 = all_24_2 % 16.51/3.11 | % 16.51/3.11 | COMBINE_EQS: (64), (65) imply: % 16.51/3.11 | (66) all_29_0 = all_24_2 % 16.51/3.11 | % 16.51/3.11 | SIMP: (66) implies: % 16.51/3.11 | (67) all_29_0 = all_24_2 % 16.51/3.11 | % 16.51/3.11 | COMBINE_EQS: (63), (67) imply: % 16.51/3.11 | (68) all_24_2 = all_22_1 % 16.51/3.11 | % 16.51/3.11 | COMBINE_EQS: (65), (68) imply: % 16.51/3.11 | (69) all_31_4 = all_22_1 % 16.51/3.11 | % 16.51/3.11 | REDUCE: (44), (69) imply: % 16.51/3.11 | (70) aDivisorOf0(xq, all_22_1) = all_31_1 % 16.51/3.11 | % 16.51/3.11 | REDUCE: (43), (69) imply: % 16.51/3.11 | (71) aDivisorOf0(xp, all_22_1) = all_31_3 % 16.51/3.11 | % 16.51/3.11 | REDUCE: (57), (63) imply: % 16.51/3.11 | (72) sdtasdt0(all_22_2, all_33_0) = all_22_1 % 16.51/3.11 | % 16.51/3.11 | REDUCE: (33), (68) imply: % 16.51/3.11 | (73) sdtasdt0(xq, all_24_0) = all_22_1 % 16.51/3.11 | % 16.51/3.11 | REDUCE: (31), (68) imply: % 16.51/3.11 | (74) sdtasdt0(xp, all_24_3) = all_22_1 % 16.51/3.11 | % 16.51/3.11 | GROUND_INST: instantiating (mIntPlus) with xa, all_22_0, all_22_1, simplifying % 16.51/3.11 | with (10), (21), (62) gives: % 16.51/3.11 | (75) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_22_0) = v1 % 16.51/3.11 | & aInteger0(all_22_1) = v2 & aInteger0(xa) = v0 & ( ~ (v1 = 0) | ~ % 16.51/3.11 | (v0 = 0) | v2 = 0)) % 16.51/3.11 | % 16.51/3.11 | GROUND_INST: instantiating (mMulComm) with xp, xq, all_22_2, simplifying with % 16.51/3.11 | (11), (12), (22) gives: % 16.51/3.11 | (76) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xq, xp) = v2 & % 16.51/3.11 | aInteger0(xq) = v1 & aInteger0(xp) = v0 & $i(v2) & ( ~ (v1 = 0) | ~ % 16.51/3.11 | (v0 = 0) | v2 = all_22_2)) % 16.51/3.11 | % 16.51/3.11 | GROUND_INST: instantiating (mIntMult) with xp, xq, all_22_2, simplifying with % 16.51/3.11 | (11), (12), (22) gives: % 16.51/3.11 | (77) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_22_2) = v2 % 16.51/3.11 | & aInteger0(xq) = v1 & aInteger0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 16.93/3.11 | 0) | v2 = 0)) % 16.93/3.11 | % 16.93/3.11 | GROUND_INST: instantiating (mMulComm) with xp, xm, all_24_0, simplifying with % 16.93/3.11 | (8), (11), (30) gives: % 16.93/3.11 | (78) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xp) = v2 & % 16.93/3.11 | aInteger0(xm) = v1 & aInteger0(xp) = v0 & $i(v2) & ( ~ (v1 = 0) | ~ % 16.93/3.11 | (v0 = 0) | v2 = all_24_0)) % 16.93/3.11 | % 16.93/3.11 | GROUND_INST: instantiating (mIntMult) with xp, xm, all_24_0, simplifying with % 16.93/3.11 | (8), (11), (30) gives: % 16.93/3.11 | (79) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_24_0) = v2 % 16.93/3.11 | & aInteger0(xm) = v1 & aInteger0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 16.93/3.11 | 0) | v2 = 0)) % 16.93/3.11 | % 16.93/3.12 | GROUND_INST: instantiating (mMulComm) with xp, all_24_3, all_22_1, simplifying % 16.93/3.12 | with (11), (25), (74) gives: % 16.93/3.12 | (80) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_24_3, xp) = % 16.93/3.12 | v2 & aInteger0(all_24_3) = v1 & aInteger0(xp) = v0 & $i(v2) & ( ~ % 16.93/3.12 | (v1 = 0) | ~ (v0 = 0) | v2 = all_22_1)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mIntMult) with xp, all_24_3, all_22_1, simplifying % 16.93/3.12 | with (11), (25), (74) gives: % 16.93/3.12 | (81) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_24_3) = v1 % 16.93/3.12 | & aInteger0(all_22_1) = v2 & aInteger0(xp) = v0 & ( ~ (v1 = 0) | ~ % 16.93/3.12 | (v0 = 0) | v2 = 0)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mMulComm) with xq, xm, all_24_3, simplifying with % 16.93/3.12 | (8), (12), (32) gives: % 16.93/3.12 | (82) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, xq) = v2 & % 16.93/3.12 | aInteger0(xm) = v1 & aInteger0(xq) = v0 & $i(v2) & ( ~ (v1 = 0) | ~ % 16.93/3.12 | (v0 = 0) | v2 = all_24_3)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mIntMult) with xq, xm, all_24_3, simplifying with % 16.93/3.12 | (8), (12), (32) gives: % 16.93/3.12 | (83) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_24_3) = v2 % 16.93/3.12 | & aInteger0(xm) = v1 & aInteger0(xq) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 16.93/3.12 | 0) | v2 = 0)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mMulComm) with xq, all_24_0, all_22_1, simplifying % 16.93/3.12 | with (12), (27), (73) gives: % 16.93/3.12 | (84) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_24_0, xq) = % 16.93/3.12 | v2 & aInteger0(all_24_0) = v1 & aInteger0(xq) = v0 & $i(v2) & ( ~ % 16.93/3.12 | (v1 = 0) | ~ (v0 = 0) | v2 = all_22_1)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mIntMult) with xq, all_24_0, all_22_1, simplifying % 16.93/3.12 | with (12), (27), (73) gives: % 16.93/3.12 | (85) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_24_0) = v1 % 16.93/3.12 | & aInteger0(all_22_1) = v2 & aInteger0(xq) = v0 & ( ~ (v1 = 0) | ~ % 16.93/3.12 | (v0 = 0) | v2 = 0)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mMulComm) with all_22_2, xm, all_22_1, simplifying % 16.93/3.12 | with (8), (23), (61) gives: % 16.93/3.12 | (86) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(xm, all_22_2) = % 16.93/3.12 | v2 & aInteger0(all_22_2) = v0 & aInteger0(xm) = v1 & $i(v2) & ( ~ % 16.93/3.12 | (v1 = 0) | ~ (v0 = 0) | v2 = all_22_1)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mIntMult) with all_22_2, xm, all_22_1, simplifying % 16.93/3.12 | with (8), (23), (61) gives: % 16.93/3.12 | (87) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_22_1) = v2 % 16.93/3.12 | & aInteger0(all_22_2) = v0 & aInteger0(xm) = v1 & ( ~ (v1 = 0) | ~ % 16.93/3.12 | (v0 = 0) | v2 = 0)) % 16.93/3.12 | % 16.93/3.12 | GROUND_INST: instantiating (mMulAsso) with xp, xq, all_33_0, all_22_2, % 16.93/3.12 | all_22_1, simplifying with (11), (12), (22), (47), (72) gives: % 16.93/3.13 | (88) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: $i] : ? [v4: $i] % 16.93/3.13 | : (sdtasdt0(xq, all_33_0) = v3 & sdtasdt0(xp, v3) = v4 & % 16.93/3.13 | aInteger0(all_33_0) = v2 & aInteger0(xq) = v1 & aInteger0(xp) = v0 & % 16.93/3.13 | $i(v4) & $i(v3) & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 16.93/3.13 | all_22_1)) % 16.93/3.13 | % 16.93/3.13 | GROUND_INST: instantiating (mMulComm) with all_22_2, all_33_0, all_22_1, % 16.93/3.13 | simplifying with (47), (61), (72) gives: % 16.93/3.13 | (89) ? [v0: any] : ? [v1: any] : ? [v2: $i] : (sdtasdt0(all_33_0, % 16.93/3.13 | all_22_2) = v2 & aInteger0(all_33_0) = v1 & aInteger0(all_22_2) = % 16.93/3.13 | v0 & $i(v2) & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_22_1)) % 16.93/3.13 | % 16.93/3.13 | GROUND_INST: instantiating (mIntMult) with all_22_2, all_33_0, all_22_1, % 16.93/3.13 | simplifying with (47), (61), (72) gives: % 16.93/3.13 | (90) ? [v0: any] : ? [v1: any] : ? [v2: any] : (aInteger0(all_33_0) = v1 % 16.93/3.13 | & aInteger0(all_22_1) = v2 & aInteger0(all_22_2) = v0 & ( ~ (v1 = 0) % 16.93/3.13 | | ~ (v0 = 0) | v2 = 0)) % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (77) with fresh symbols all_60_0, all_60_1, all_60_2 % 16.93/3.13 | gives: % 16.93/3.13 | (91) aInteger0(all_22_2) = all_60_0 & aInteger0(xq) = all_60_1 & % 16.93/3.13 | aInteger0(xp) = all_60_2 & ( ~ (all_60_1 = 0) | ~ (all_60_2 = 0) | % 16.93/3.13 | all_60_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (91) implies: % 16.93/3.13 | (92) aInteger0(xp) = all_60_2 % 16.93/3.13 | (93) aInteger0(xq) = all_60_1 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (75) with fresh symbols all_62_0, all_62_1, all_62_2 % 16.93/3.13 | gives: % 16.93/3.13 | (94) aInteger0(all_22_0) = all_62_1 & aInteger0(all_22_1) = all_62_0 & % 16.93/3.13 | aInteger0(xa) = all_62_2 & ( ~ (all_62_1 = 0) | ~ (all_62_2 = 0) | % 16.93/3.13 | all_62_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (94) implies: % 16.93/3.13 | (95) aInteger0(all_22_1) = all_62_0 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (90) with fresh symbols all_64_0, all_64_1, all_64_2 % 16.93/3.13 | gives: % 16.93/3.13 | (96) aInteger0(all_33_0) = all_64_1 & aInteger0(all_22_1) = all_64_0 & % 16.93/3.13 | aInteger0(all_22_2) = all_64_2 & ( ~ (all_64_1 = 0) | ~ (all_64_2 = % 16.93/3.13 | 0) | all_64_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (96) implies: % 16.93/3.13 | (97) aInteger0(all_22_1) = all_64_0 % 16.93/3.13 | (98) aInteger0(all_33_0) = all_64_1 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (87) with fresh symbols all_66_0, all_66_1, all_66_2 % 16.93/3.13 | gives: % 16.93/3.13 | (99) aInteger0(all_22_1) = all_66_0 & aInteger0(all_22_2) = all_66_2 & % 16.93/3.13 | aInteger0(xm) = all_66_1 & ( ~ (all_66_1 = 0) | ~ (all_66_2 = 0) | % 16.93/3.13 | all_66_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (99) implies: % 16.93/3.13 | (100) aInteger0(all_22_1) = all_66_0 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (85) with fresh symbols all_68_0, all_68_1, all_68_2 % 16.93/3.13 | gives: % 16.93/3.13 | (101) aInteger0(all_24_0) = all_68_1 & aInteger0(all_22_1) = all_68_0 & % 16.93/3.13 | aInteger0(xq) = all_68_2 & ( ~ (all_68_1 = 0) | ~ (all_68_2 = 0) | % 16.93/3.13 | all_68_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (101) implies: % 16.93/3.13 | (102) aInteger0(xq) = all_68_2 % 16.93/3.13 | (103) aInteger0(all_22_1) = all_68_0 % 16.93/3.13 | (104) aInteger0(all_24_0) = all_68_1 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (83) with fresh symbols all_70_0, all_70_1, all_70_2 % 16.93/3.13 | gives: % 16.93/3.13 | (105) aInteger0(all_24_3) = all_70_0 & aInteger0(xm) = all_70_1 & % 16.93/3.13 | aInteger0(xq) = all_70_2 & ( ~ (all_70_1 = 0) | ~ (all_70_2 = 0) | % 16.93/3.13 | all_70_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (105) implies: % 16.93/3.13 | (106) aInteger0(xq) = all_70_2 % 16.93/3.13 | (107) aInteger0(xm) = all_70_1 % 16.93/3.13 | (108) aInteger0(all_24_3) = all_70_0 % 16.93/3.13 | (109) ~ (all_70_1 = 0) | ~ (all_70_2 = 0) | all_70_0 = 0 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (81) with fresh symbols all_72_0, all_72_1, all_72_2 % 16.93/3.13 | gives: % 16.93/3.13 | (110) aInteger0(all_24_3) = all_72_1 & aInteger0(all_22_1) = all_72_0 & % 16.93/3.13 | aInteger0(xp) = all_72_2 & ( ~ (all_72_1 = 0) | ~ (all_72_2 = 0) | % 16.93/3.13 | all_72_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (110) implies: % 16.93/3.13 | (111) aInteger0(xp) = all_72_2 % 16.93/3.13 | (112) aInteger0(all_22_1) = all_72_0 % 16.93/3.13 | (113) aInteger0(all_24_3) = all_72_1 % 16.93/3.13 | (114) ~ (all_72_1 = 0) | ~ (all_72_2 = 0) | all_72_0 = 0 % 16.93/3.13 | % 16.93/3.13 | DELTA: instantiating (79) with fresh symbols all_74_0, all_74_1, all_74_2 % 16.93/3.13 | gives: % 16.93/3.13 | (115) aInteger0(all_24_0) = all_74_0 & aInteger0(xm) = all_74_1 & % 16.93/3.13 | aInteger0(xp) = all_74_2 & ( ~ (all_74_1 = 0) | ~ (all_74_2 = 0) | % 16.93/3.13 | all_74_0 = 0) % 16.93/3.13 | % 16.93/3.13 | ALPHA: (115) implies: % 16.93/3.14 | (116) aInteger0(xp) = all_74_2 % 16.93/3.14 | (117) aInteger0(xm) = all_74_1 % 16.93/3.14 | (118) aInteger0(all_24_0) = all_74_0 % 16.93/3.14 | (119) ~ (all_74_1 = 0) | ~ (all_74_2 = 0) | all_74_0 = 0 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (89) with fresh symbols all_76_0, all_76_1, all_76_2 % 16.93/3.14 | gives: % 16.93/3.14 | (120) sdtasdt0(all_33_0, all_22_2) = all_76_0 & aInteger0(all_33_0) = % 16.93/3.14 | all_76_1 & aInteger0(all_22_2) = all_76_2 & $i(all_76_0) & ( ~ % 16.93/3.14 | (all_76_1 = 0) | ~ (all_76_2 = 0) | all_76_0 = all_22_1) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (120) implies: % 16.93/3.14 | (121) aInteger0(all_33_0) = all_76_1 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (78) with fresh symbols all_78_0, all_78_1, all_78_2 % 16.93/3.14 | gives: % 16.93/3.14 | (122) sdtasdt0(xm, xp) = all_78_0 & aInteger0(xm) = all_78_1 & % 16.93/3.14 | aInteger0(xp) = all_78_2 & $i(all_78_0) & ( ~ (all_78_1 = 0) | ~ % 16.93/3.14 | (all_78_2 = 0) | all_78_0 = all_24_0) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (122) implies: % 16.93/3.14 | (123) aInteger0(xp) = all_78_2 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (80) with fresh symbols all_82_0, all_82_1, all_82_2 % 16.93/3.14 | gives: % 16.93/3.14 | (124) sdtasdt0(all_24_3, xp) = all_82_0 & aInteger0(all_24_3) = all_82_1 & % 16.93/3.14 | aInteger0(xp) = all_82_2 & $i(all_82_0) & ( ~ (all_82_1 = 0) | ~ % 16.93/3.14 | (all_82_2 = 0) | all_82_0 = all_22_1) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (124) implies: % 16.93/3.14 | (125) aInteger0(xp) = all_82_2 % 16.93/3.14 | (126) aInteger0(all_24_3) = all_82_1 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (76) with fresh symbols all_84_0, all_84_1, all_84_2 % 16.93/3.14 | gives: % 16.93/3.14 | (127) sdtasdt0(xq, xp) = all_84_0 & aInteger0(xq) = all_84_1 & % 16.93/3.14 | aInteger0(xp) = all_84_2 & $i(all_84_0) & ( ~ (all_84_1 = 0) | ~ % 16.93/3.14 | (all_84_2 = 0) | all_84_0 = all_22_2) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (127) implies: % 16.93/3.14 | (128) aInteger0(xp) = all_84_2 % 16.93/3.14 | (129) aInteger0(xq) = all_84_1 % 16.93/3.14 | (130) sdtasdt0(xq, xp) = all_84_0 % 16.93/3.14 | (131) ~ (all_84_1 = 0) | ~ (all_84_2 = 0) | all_84_0 = all_22_2 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (84) with fresh symbols all_86_0, all_86_1, all_86_2 % 16.93/3.14 | gives: % 16.93/3.14 | (132) sdtasdt0(all_24_0, xq) = all_86_0 & aInteger0(all_24_0) = all_86_1 & % 16.93/3.14 | aInteger0(xq) = all_86_2 & $i(all_86_0) & ( ~ (all_86_1 = 0) | ~ % 16.93/3.14 | (all_86_2 = 0) | all_86_0 = all_22_1) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (132) implies: % 16.93/3.14 | (133) $i(all_86_0) % 16.93/3.14 | (134) aInteger0(xq) = all_86_2 % 16.93/3.14 | (135) aInteger0(all_24_0) = all_86_1 % 16.93/3.14 | (136) ~ (all_86_1 = 0) | ~ (all_86_2 = 0) | all_86_0 = all_22_1 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (86) with fresh symbols all_88_0, all_88_1, all_88_2 % 16.93/3.14 | gives: % 16.93/3.14 | (137) sdtasdt0(xm, all_22_2) = all_88_0 & aInteger0(all_22_2) = all_88_2 & % 16.93/3.14 | aInteger0(xm) = all_88_1 & $i(all_88_0) & ( ~ (all_88_1 = 0) | ~ % 16.93/3.14 | (all_88_2 = 0) | all_88_0 = all_22_1) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (137) implies: % 16.93/3.14 | (138) aInteger0(xm) = all_88_1 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (82) with fresh symbols all_90_0, all_90_1, all_90_2 % 16.93/3.14 | gives: % 16.93/3.14 | (139) sdtasdt0(xm, xq) = all_90_0 & aInteger0(xm) = all_90_1 & % 16.93/3.14 | aInteger0(xq) = all_90_2 & $i(all_90_0) & ( ~ (all_90_1 = 0) | ~ % 16.93/3.14 | (all_90_2 = 0) | all_90_0 = all_24_3) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (139) implies: % 16.93/3.14 | (140) aInteger0(xq) = all_90_2 % 16.93/3.14 | (141) aInteger0(xm) = all_90_1 % 16.93/3.14 | % 16.93/3.14 | DELTA: instantiating (88) with fresh symbols all_92_0, all_92_1, all_92_2, % 16.93/3.14 | all_92_3, all_92_4 gives: % 16.93/3.14 | (142) sdtasdt0(xq, all_33_0) = all_92_1 & sdtasdt0(xp, all_92_1) = all_92_0 % 16.93/3.14 | & aInteger0(all_33_0) = all_92_2 & aInteger0(xq) = all_92_3 & % 16.93/3.14 | aInteger0(xp) = all_92_4 & $i(all_92_0) & $i(all_92_1) & ( ~ % 16.93/3.14 | (all_92_2 = 0) | ~ (all_92_3 = 0) | ~ (all_92_4 = 0) | all_92_0 = % 16.93/3.14 | all_22_1) % 16.93/3.14 | % 16.93/3.14 | ALPHA: (142) implies: % 16.93/3.14 | (143) $i(all_92_1) % 16.93/3.14 | (144) aInteger0(xp) = all_92_4 % 16.93/3.14 | (145) aInteger0(xq) = all_92_3 % 16.93/3.14 | (146) aInteger0(all_33_0) = all_92_2 % 16.93/3.14 | (147) sdtasdt0(xp, all_92_1) = all_92_0 % 16.93/3.14 | (148) sdtasdt0(xq, all_33_0) = all_92_1 % 16.93/3.14 | (149) ~ (all_92_2 = 0) | ~ (all_92_3 = 0) | ~ (all_92_4 = 0) | all_92_0 % 16.93/3.14 | = all_22_1 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with all_60_2, all_78_2, xp, simplifying with % 16.93/3.14 | (92), (123) gives: % 16.93/3.14 | (150) all_78_2 = all_60_2 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with all_78_2, all_82_2, xp, simplifying with % 16.93/3.14 | (123), (125) gives: % 16.93/3.14 | (151) all_82_2 = all_78_2 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with 0, all_84_2, xp, simplifying with (4), % 16.93/3.14 | (128) gives: % 16.93/3.14 | (152) all_84_2 = 0 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with all_82_2, all_84_2, xp, simplifying with % 16.93/3.14 | (125), (128) gives: % 16.93/3.14 | (153) all_84_2 = all_82_2 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with all_72_2, all_84_2, xp, simplifying with % 16.93/3.14 | (111), (128) gives: % 16.93/3.14 | (154) all_84_2 = all_72_2 % 16.93/3.14 | % 16.93/3.14 | GROUND_INST: instantiating (14) with all_82_2, all_92_4, xp, simplifying with % 16.93/3.14 | (125), (144) gives: % 16.93/3.14 | (155) all_92_4 = all_82_2 % 16.93/3.14 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_74_2, all_92_4, xp, simplifying with % 16.93/3.15 | (116), (144) gives: % 16.93/3.15 | (156) all_92_4 = all_74_2 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with 0, all_86_2, xq, simplifying with (5), % 16.93/3.15 | (134) gives: % 16.93/3.15 | (157) all_86_2 = 0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_68_2, all_86_2, xq, simplifying with % 16.93/3.15 | (102), (134) gives: % 16.93/3.15 | (158) all_86_2 = all_68_2 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_86_2, all_90_2, xq, simplifying with % 16.93/3.15 | (134), (140) gives: % 16.93/3.15 | (159) all_90_2 = all_86_2 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_84_1, all_90_2, xq, simplifying with % 16.93/3.15 | (129), (140) gives: % 16.93/3.15 | (160) all_90_2 = all_84_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_60_1, all_90_2, xq, simplifying with % 16.93/3.15 | (93), (140) gives: % 16.93/3.15 | (161) all_90_2 = all_60_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_90_2, all_92_3, xq, simplifying with % 16.93/3.15 | (140), (145) gives: % 16.93/3.15 | (162) all_92_3 = all_90_2 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_70_2, all_92_3, xq, simplifying with % 16.93/3.15 | (106), (145) gives: % 16.93/3.15 | (163) all_92_3 = all_70_2 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_74_1, all_88_1, xm, simplifying with % 16.93/3.15 | (117), (138) gives: % 16.93/3.15 | (164) all_88_1 = all_74_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_70_1, all_88_1, xm, simplifying with % 16.93/3.15 | (107), (138) gives: % 16.93/3.15 | (165) all_88_1 = all_70_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with 0, all_90_1, xm, simplifying with (19), % 16.93/3.15 | (141) gives: % 16.93/3.15 | (166) all_90_1 = 0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_88_1, all_90_1, xm, simplifying with % 16.93/3.15 | (138), (141) gives: % 16.93/3.15 | (167) all_90_1 = all_88_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_64_0, all_66_0, all_22_1, simplifying % 16.93/3.15 | with (97), (100) gives: % 16.93/3.15 | (168) all_66_0 = all_64_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_68_0, all_72_0, all_22_1, simplifying % 16.93/3.15 | with (103), (112) gives: % 16.93/3.15 | (169) all_72_0 = all_68_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_66_0, all_72_0, all_22_1, simplifying % 16.93/3.15 | with (100), (112) gives: % 16.93/3.15 | (170) all_72_0 = all_66_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_62_0, all_72_0, all_22_1, simplifying % 16.93/3.15 | with (95), (112) gives: % 16.93/3.15 | (171) all_72_0 = all_62_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_72_1, all_82_1, all_24_3, simplifying % 16.93/3.15 | with (113), (126) gives: % 16.93/3.15 | (172) all_82_1 = all_72_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_70_0, all_82_1, all_24_3, simplifying % 16.93/3.15 | with (108), (126) gives: % 16.93/3.15 | (173) all_82_1 = all_70_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_74_0, all_86_1, all_24_0, simplifying % 16.93/3.15 | with (118), (135) gives: % 16.93/3.15 | (174) all_86_1 = all_74_0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_68_1, all_86_1, all_24_0, simplifying % 16.93/3.15 | with (104), (135) gives: % 16.93/3.15 | (175) all_86_1 = all_68_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_64_1, all_76_1, all_33_0, simplifying % 16.93/3.15 | with (98), (121) gives: % 16.93/3.15 | (176) all_76_1 = all_64_1 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with 0, all_92_2, all_33_0, simplifying with % 16.93/3.15 | (48), (146) gives: % 16.93/3.15 | (177) all_92_2 = 0 % 16.93/3.15 | % 16.93/3.15 | GROUND_INST: instantiating (14) with all_76_1, all_92_2, all_33_0, simplifying % 16.93/3.15 | with (121), (146) gives: % 16.93/3.15 | (178) all_92_2 = all_76_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (177), (178) imply: % 16.93/3.15 | (179) all_76_1 = 0 % 16.93/3.15 | % 16.93/3.15 | SIMP: (179) implies: % 16.93/3.15 | (180) all_76_1 = 0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (162), (163) imply: % 16.93/3.15 | (181) all_90_2 = all_70_2 % 16.93/3.15 | % 16.93/3.15 | SIMP: (181) implies: % 16.93/3.15 | (182) all_90_2 = all_70_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (155), (156) imply: % 16.93/3.15 | (183) all_82_2 = all_74_2 % 16.93/3.15 | % 16.93/3.15 | SIMP: (183) implies: % 16.93/3.15 | (184) all_82_2 = all_74_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (166), (167) imply: % 16.93/3.15 | (185) all_88_1 = 0 % 16.93/3.15 | % 16.93/3.15 | SIMP: (185) implies: % 16.93/3.15 | (186) all_88_1 = 0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (159), (160) imply: % 16.93/3.15 | (187) all_86_2 = all_84_1 % 16.93/3.15 | % 16.93/3.15 | SIMP: (187) implies: % 16.93/3.15 | (188) all_86_2 = all_84_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (160), (161) imply: % 16.93/3.15 | (189) all_84_1 = all_60_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (160), (182) imply: % 16.93/3.15 | (190) all_84_1 = all_70_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (164), (186) imply: % 16.93/3.15 | (191) all_74_1 = 0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (164), (165) imply: % 16.93/3.15 | (192) all_74_1 = all_70_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (174), (175) imply: % 16.93/3.15 | (193) all_74_0 = all_68_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (157), (158) imply: % 16.93/3.15 | (194) all_68_2 = 0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (158), (188) imply: % 16.93/3.15 | (195) all_84_1 = all_68_2 % 16.93/3.15 | % 16.93/3.15 | SIMP: (195) implies: % 16.93/3.15 | (196) all_84_1 = all_68_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (189), (190) imply: % 16.93/3.15 | (197) all_70_2 = all_60_1 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (190), (196) imply: % 16.93/3.15 | (198) all_70_2 = all_68_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (152), (154) imply: % 16.93/3.15 | (199) all_72_2 = 0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (153), (154) imply: % 16.93/3.15 | (200) all_82_2 = all_72_2 % 16.93/3.15 | % 16.93/3.15 | SIMP: (200) implies: % 16.93/3.15 | (201) all_82_2 = all_72_2 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (172), (173) imply: % 16.93/3.15 | (202) all_72_1 = all_70_0 % 16.93/3.15 | % 16.93/3.15 | SIMP: (202) implies: % 16.93/3.15 | (203) all_72_1 = all_70_0 % 16.93/3.15 | % 16.93/3.15 | COMBINE_EQS: (151), (184) imply: % 16.93/3.15 | (204) all_78_2 = all_74_2 % 16.93/3.15 | % 16.93/3.15 | SIMP: (204) implies: % 16.93/3.15 | (205) all_78_2 = all_74_2 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (184), (201) imply: % 16.93/3.16 | (206) all_74_2 = all_72_2 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (150), (205) imply: % 16.93/3.16 | (207) all_74_2 = all_60_2 % 16.93/3.16 | % 16.93/3.16 | SIMP: (207) implies: % 16.93/3.16 | (208) all_74_2 = all_60_2 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (176), (180) imply: % 16.93/3.16 | (209) all_64_1 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (191), (192) imply: % 16.93/3.16 | (210) all_70_1 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (206), (208) imply: % 16.93/3.16 | (211) all_72_2 = all_60_2 % 16.93/3.16 | % 16.93/3.16 | SIMP: (211) implies: % 16.93/3.16 | (212) all_72_2 = all_60_2 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (169), (171) imply: % 16.93/3.16 | (213) all_68_0 = all_62_0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (169), (170) imply: % 16.93/3.16 | (214) all_68_0 = all_66_0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (199), (212) imply: % 16.93/3.16 | (215) all_60_2 = 0 % 16.93/3.16 | % 16.93/3.16 | SIMP: (215) implies: % 16.93/3.16 | (216) all_60_2 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (197), (198) imply: % 16.93/3.16 | (217) all_68_2 = all_60_1 % 16.93/3.16 | % 16.93/3.16 | SIMP: (217) implies: % 16.93/3.16 | (218) all_68_2 = all_60_1 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (213), (214) imply: % 16.93/3.16 | (219) all_66_0 = all_62_0 % 16.93/3.16 | % 16.93/3.16 | SIMP: (219) implies: % 16.93/3.16 | (220) all_66_0 = all_62_0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (194), (218) imply: % 16.93/3.16 | (221) all_60_1 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (168), (220) imply: % 16.93/3.16 | (222) all_64_0 = all_62_0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (197), (221) imply: % 16.93/3.16 | (223) all_70_2 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (208), (216) imply: % 16.93/3.16 | (224) all_74_2 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (190), (223) imply: % 16.93/3.16 | (225) all_84_1 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (156), (224) imply: % 16.93/3.16 | (226) all_92_4 = 0 % 16.93/3.16 | % 16.93/3.16 | COMBINE_EQS: (163), (223) imply: % 16.93/3.16 | (227) all_92_3 = 0 % 16.93/3.16 | % 16.93/3.16 | BETA: splitting (109) gives: % 16.93/3.16 | % 16.93/3.16 | Case 1: % 16.93/3.16 | | % 16.93/3.16 | | (228) ~ (all_70_1 = 0) % 16.93/3.16 | | % 16.93/3.16 | | REDUCE: (210), (228) imply: % 16.93/3.16 | | (229) $false % 16.93/3.16 | | % 16.93/3.16 | | CLOSE: (229) is inconsistent. % 16.93/3.16 | | % 16.93/3.16 | Case 2: % 16.93/3.16 | | % 16.93/3.16 | | (230) ~ (all_70_2 = 0) | all_70_0 = 0 % 16.93/3.16 | | % 16.93/3.16 | | BETA: splitting (230) gives: % 16.93/3.16 | | % 16.93/3.16 | | Case 1: % 16.93/3.16 | | | % 16.93/3.16 | | | (231) ~ (all_70_2 = 0) % 16.93/3.16 | | | % 16.93/3.16 | | | REDUCE: (223), (231) imply: % 16.93/3.16 | | | (232) $false % 16.93/3.16 | | | % 16.93/3.16 | | | CLOSE: (232) is inconsistent. % 16.93/3.16 | | | % 16.93/3.16 | | Case 2: % 16.93/3.16 | | | % 16.93/3.16 | | | (233) all_70_0 = 0 % 16.93/3.16 | | | % 16.93/3.16 | | | COMBINE_EQS: (203), (233) imply: % 16.93/3.16 | | | (234) all_72_1 = 0 % 16.93/3.16 | | | % 16.93/3.16 | | | BETA: splitting (114) gives: % 16.93/3.16 | | | % 16.93/3.16 | | | Case 1: % 16.93/3.16 | | | | % 16.93/3.16 | | | | (235) ~ (all_72_1 = 0) % 16.93/3.16 | | | | % 16.93/3.16 | | | | REDUCE: (234), (235) imply: % 16.93/3.16 | | | | (236) $false % 16.93/3.16 | | | | % 16.93/3.16 | | | | CLOSE: (236) is inconsistent. % 16.93/3.16 | | | | % 16.93/3.16 | | | Case 2: % 16.93/3.16 | | | | % 16.93/3.16 | | | | (237) ~ (all_72_2 = 0) | all_72_0 = 0 % 16.93/3.16 | | | | % 16.93/3.16 | | | | BETA: splitting (237) gives: % 16.93/3.16 | | | | % 16.93/3.16 | | | | Case 1: % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | (238) ~ (all_72_2 = 0) % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | REDUCE: (199), (238) imply: % 16.93/3.16 | | | | | (239) $false % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | CLOSE: (239) is inconsistent. % 16.93/3.16 | | | | | % 16.93/3.16 | | | | Case 2: % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | (240) all_72_0 = 0 % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | COMBINE_EQS: (171), (240) imply: % 16.93/3.16 | | | | | (241) all_62_0 = 0 % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | SIMP: (241) implies: % 16.93/3.16 | | | | | (242) all_62_0 = 0 % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | REDUCE: (95), (242) imply: % 16.93/3.16 | | | | | (243) aInteger0(all_22_1) = 0 % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | BETA: splitting (119) gives: % 16.93/3.16 | | | | | % 16.93/3.16 | | | | | Case 1: % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | (244) ~ (all_74_1 = 0) % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | REDUCE: (191), (244) imply: % 16.93/3.16 | | | | | | (245) $false % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | CLOSE: (245) is inconsistent. % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | Case 2: % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | (246) ~ (all_74_2 = 0) | all_74_0 = 0 % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | BETA: splitting (149) gives: % 16.93/3.16 | | | | | | % 16.93/3.16 | | | | | | Case 1: % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | (247) ~ (all_92_2 = 0) % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | REDUCE: (177), (247) imply: % 16.93/3.16 | | | | | | | (248) $false % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | CLOSE: (248) is inconsistent. % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | Case 2: % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | (249) ~ (all_92_3 = 0) | ~ (all_92_4 = 0) | all_92_0 = % 16.93/3.16 | | | | | | | all_22_1 % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | BETA: splitting (249) gives: % 16.93/3.16 | | | | | | | % 16.93/3.16 | | | | | | | Case 1: % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | (250) ~ (all_92_3 = 0) % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | REDUCE: (227), (250) imply: % 16.93/3.16 | | | | | | | | (251) $false % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | CLOSE: (251) is inconsistent. % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | Case 2: % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | (252) ~ (all_92_4 = 0) | all_92_0 = all_22_1 % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | BETA: splitting (131) gives: % 16.93/3.16 | | | | | | | | % 16.93/3.16 | | | | | | | | Case 1: % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | (253) ~ (all_84_1 = 0) % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | REDUCE: (225), (253) imply: % 16.93/3.16 | | | | | | | | | (254) $false % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | CLOSE: (254) is inconsistent. % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | Case 2: % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | (255) ~ (all_84_2 = 0) | all_84_0 = all_22_2 % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | BETA: splitting (255) gives: % 16.93/3.16 | | | | | | | | | % 16.93/3.16 | | | | | | | | | Case 1: % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | (256) ~ (all_84_2 = 0) % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | REDUCE: (152), (256) imply: % 16.93/3.16 | | | | | | | | | | (257) $false % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | CLOSE: (257) is inconsistent. % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | Case 2: % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | (258) all_84_0 = all_22_2 % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | REDUCE: (130), (258) imply: % 16.93/3.16 | | | | | | | | | | (259) sdtasdt0(xq, xp) = all_22_2 % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | BETA: splitting (246) gives: % 16.93/3.16 | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | Case 1: % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | (260) ~ (all_74_2 = 0) % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | REDUCE: (224), (260) imply: % 16.93/3.16 | | | | | | | | | | | (261) $false % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | CLOSE: (261) is inconsistent. % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | Case 2: % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | (262) all_74_0 = 0 % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | COMBINE_EQS: (193), (262) imply: % 16.93/3.16 | | | | | | | | | | | (263) all_68_1 = 0 % 16.93/3.16 | | | | | | | | | | | % 16.93/3.16 | | | | | | | | | | | SIMP: (263) implies: % 16.93/3.17 | | | | | | | | | | | (264) all_68_1 = 0 % 16.93/3.17 | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | COMBINE_EQS: (175), (264) imply: % 16.93/3.17 | | | | | | | | | | | (265) all_86_1 = 0 % 16.93/3.17 | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | REDUCE: (104), (264) imply: % 16.93/3.17 | | | | | | | | | | | (266) aInteger0(all_24_0) = 0 % 16.93/3.17 | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | BETA: splitting (252) gives: % 16.93/3.17 | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | Case 1: % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | (267) ~ (all_92_4 = 0) % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | REDUCE: (226), (267) imply: % 16.93/3.17 | | | | | | | | | | | | (268) $false % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | CLOSE: (268) is inconsistent. % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | Case 2: % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | (269) all_92_0 = all_22_1 % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | REDUCE: (147), (269) imply: % 16.93/3.17 | | | | | | | | | | | | (270) sdtasdt0(xp, all_92_1) = all_22_1 % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | BETA: splitting (136) gives: % 16.93/3.17 | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | Case 1: % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | (271) ~ (all_86_1 = 0) % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | REDUCE: (265), (271) imply: % 16.93/3.17 | | | | | | | | | | | | | (272) $false % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | CLOSE: (272) is inconsistent. % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | Case 2: % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | (273) ~ (all_86_2 = 0) | all_86_0 = all_22_1 % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | BETA: splitting (273) gives: % 16.93/3.17 | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | Case 1: % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | (274) ~ (all_86_2 = 0) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | REDUCE: (157), (274) imply: % 16.93/3.17 | | | | | | | | | | | | | | (275) $false % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | CLOSE: (275) is inconsistent. % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | Case 2: % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | (276) all_86_0 = all_22_1 % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | REDUCE: (133), (276) imply: % 16.93/3.17 | | | | | | | | | | | | | | (277) $i(all_22_1) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (1) with all_22_1, simplifying with % 16.93/3.17 | | | | | | | | | | | | | | (243), (277) gives: % 16.93/3.17 | | | | | | | | | | | | | | (278) ! [v0: $i] : ! [v1: int] : (v1 = 0 | v0 = sz00 | % 16.93/3.17 | | | | | | | | | | | | | | ~ (aDivisorOf0(v0, all_22_1) = v1) | ~ $i(v0) % 16.93/3.17 | | | | | | | | | | | | | | | ? [v2: int] : ( ~ (v2 = 0) & aInteger0(v0) = % 16.93/3.17 | | | | | | | | | | | | | | v2) | ! [v2: $i] : ( ~ (sdtasdt0(v0, v2) = % 16.93/3.17 | | | | | | | | | | | | | | all_22_1) | ~ $i(v2) | ? [v3: int] : ( ~ % 16.93/3.17 | | | | | | | | | | | | | | (v3 = 0) & aInteger0(v2) = v3))) & ! [v0: % 16.93/3.17 | | | | | | | | | | | | | | $i] : ( ~ (aDivisorOf0(v0, all_22_1) = 0) | ~ % 16.93/3.17 | | | | | | | | | | | | | | $i(v0) | ( ~ (v0 = sz00) & aInteger0(v0) = 0 & % 16.93/3.17 | | | | | | | | | | | | | | ? [v1: $i] : (sdtasdt0(v0, v1) = all_22_1 & % 16.93/3.17 | | | | | | | | | | | | | | aInteger0(v1) = 0 & $i(v1)))) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | ALPHA: (278) implies: % 16.93/3.17 | | | | | | | | | | | | | | (279) ! [v0: $i] : ! [v1: int] : (v1 = 0 | v0 = sz00 | % 16.93/3.17 | | | | | | | | | | | | | | ~ (aDivisorOf0(v0, all_22_1) = v1) | ~ $i(v0) % 16.93/3.17 | | | | | | | | | | | | | | | ? [v2: int] : ( ~ (v2 = 0) & aInteger0(v0) = % 16.93/3.17 | | | | | | | | | | | | | | v2) | ! [v2: $i] : ( ~ (sdtasdt0(v0, v2) = % 16.93/3.17 | | | | | | | | | | | | | | all_22_1) | ~ $i(v2) | ? [v3: int] : ( ~ % 16.93/3.17 | | | | | | | | | | | | | | (v3 = 0) & aInteger0(v2) = v3))) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xp, all_92_1, % 16.93/3.17 | | | | | | | | | | | | | | all_22_1, simplifying with (11), (143), (270) % 16.93/3.17 | | | | | | | | | | | | | | gives: % 16.93/3.17 | | | | | | | | | | | | | | (280) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 16.93/3.17 | | | | | | | | | | | | | | (sdtasdt0(all_92_1, xp) = v2 & aInteger0(all_92_1) % 16.93/3.17 | | | | | | | | | | | | | | = v1 & aInteger0(xp) = v0 & $i(v2) & ( ~ (v1 = % 16.93/3.17 | | | | | | | | | | | | | | 0) | ~ (v0 = 0) | v2 = all_22_1)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (mIntMult) with xp, all_92_1, % 16.93/3.17 | | | | | | | | | | | | | | all_22_1, simplifying with (11), (143), (270) % 16.93/3.17 | | | | | | | | | | | | | | gives: % 16.93/3.17 | | | | | | | | | | | | | | (281) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 16.93/3.17 | | | | | | | | | | | | | | (aInteger0(all_92_1) = v1 & aInteger0(all_22_1) = % 16.93/3.17 | | | | | | | | | | | | | | v2 & aInteger0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 % 16.93/3.17 | | | | | | | | | | | | | | = 0) | v2 = 0)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulAsso) with xq, xp, all_33_0, % 16.93/3.17 | | | | | | | | | | | | | | all_22_2, all_22_1, simplifying with (11), (12), % 16.93/3.17 | | | | | | | | | | | | | | (47), (72), (259) gives: % 16.93/3.17 | | | | | | | | | | | | | | (282) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 16.93/3.17 | | | | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (sdtasdt0(xq, v3) = v4 & % 16.93/3.17 | | | | | | | | | | | | | | sdtasdt0(xp, all_33_0) = v3 & % 16.93/3.17 | | | | | | | | | | | | | | aInteger0(all_33_0) = v2 & aInteger0(xq) = v0 & % 16.93/3.17 | | | | | | | | | | | | | | aInteger0(xp) = v1 & $i(v4) & $i(v3) & ( ~ (v2 = % 16.93/3.17 | | | | | | | | | | | | | | 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 16.93/3.17 | | | | | | | | | | | | | | all_22_1)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (mMulComm) with xq, all_33_0, % 16.93/3.17 | | | | | | | | | | | | | | all_92_1, simplifying with (12), (47), (148) % 16.93/3.17 | | | | | | | | | | | | | | gives: % 16.93/3.17 | | | | | | | | | | | | | | (283) ? [v0: any] : ? [v1: any] : ? [v2: $i] : % 16.93/3.17 | | | | | | | | | | | | | | (sdtasdt0(all_33_0, xq) = v2 & aInteger0(all_33_0) % 16.93/3.17 | | | | | | | | | | | | | | = v1 & aInteger0(xq) = v0 & $i(v2) & ( ~ (v1 = % 16.93/3.17 | | | | | | | | | | | | | | 0) | ~ (v0 = 0) | v2 = all_92_1)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (mIntMult) with xq, all_33_0, % 16.93/3.17 | | | | | | | | | | | | | | all_92_1, simplifying with (12), (47), (148) % 16.93/3.17 | | | | | | | | | | | | | | gives: % 16.93/3.17 | | | | | | | | | | | | | | (284) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 16.93/3.17 | | | | | | | | | | | | | | (aInteger0(all_92_1) = v2 & aInteger0(all_33_0) = % 16.93/3.17 | | | | | | | | | | | | | | v1 & aInteger0(xq) = v0 & ( ~ (v1 = 0) | ~ (v0 % 16.93/3.17 | | | | | | | | | | | | | | = 0) | v2 = 0)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (279) with xp, all_31_3, simplifying % 16.93/3.17 | | | | | | | | | | | | | | with (11), (71) gives: % 16.93/3.17 | | | | | | | | | | | | | | (285) all_31_3 = 0 | xp = sz00 | ? [v0: int] : ( ~ (v0 % 16.93/3.17 | | | | | | | | | | | | | | = 0) & aInteger0(xp) = v0) | ! [v0: $i] : ( ~ % 16.93/3.17 | | | | | | | | | | | | | | (sdtasdt0(xp, v0) = all_22_1) | ~ $i(v0) | ? % 16.93/3.17 | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | GROUND_INST: instantiating (279) with xq, all_31_1, simplifying % 16.93/3.17 | | | | | | | | | | | | | | with (12), (70) gives: % 16.93/3.17 | | | | | | | | | | | | | | (286) all_31_1 = 0 | xq = sz00 | ? [v0: int] : ( ~ (v0 % 16.93/3.17 | | | | | | | | | | | | | | = 0) & aInteger0(xq) = v0) | ! [v0: $i] : ( ~ % 16.93/3.17 | | | | | | | | | | | | | | (sdtasdt0(xq, v0) = all_22_1) | ~ $i(v0) | ? % 16.93/3.17 | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1)) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | DELTA: instantiating (281) with fresh symbols all_248_0, % 16.93/3.17 | | | | | | | | | | | | | | all_248_1, all_248_2 gives: % 16.93/3.17 | | | | | | | | | | | | | | (287) aInteger0(all_92_1) = all_248_1 & % 16.93/3.17 | | | | | | | | | | | | | | aInteger0(all_22_1) = all_248_0 & aInteger0(xp) = % 16.93/3.17 | | | | | | | | | | | | | | all_248_2 & ( ~ (all_248_1 = 0) | ~ (all_248_2 = % 16.93/3.17 | | | | | | | | | | | | | | 0) | all_248_0 = 0) % 16.93/3.17 | | | | | | | | | | | | | | % 16.93/3.17 | | | | | | | | | | | | | | ALPHA: (287) implies: % 16.93/3.18 | | | | | | | | | | | | | | (288) aInteger0(xp) = all_248_2 % 16.93/3.18 | | | | | | | | | | | | | | (289) aInteger0(all_92_1) = all_248_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | DELTA: instantiating (284) with fresh symbols all_250_0, % 16.93/3.18 | | | | | | | | | | | | | | all_250_1, all_250_2 gives: % 16.93/3.18 | | | | | | | | | | | | | | (290) aInteger0(all_92_1) = all_250_0 & % 16.93/3.18 | | | | | | | | | | | | | | aInteger0(all_33_0) = all_250_1 & aInteger0(xq) = % 16.93/3.18 | | | | | | | | | | | | | | all_250_2 & ( ~ (all_250_1 = 0) | ~ (all_250_2 = % 16.93/3.18 | | | | | | | | | | | | | | 0) | all_250_0 = 0) % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | ALPHA: (290) implies: % 16.93/3.18 | | | | | | | | | | | | | | (291) aInteger0(xq) = all_250_2 % 16.93/3.18 | | | | | | | | | | | | | | (292) aInteger0(all_33_0) = all_250_1 % 16.93/3.18 | | | | | | | | | | | | | | (293) aInteger0(all_92_1) = all_250_0 % 16.93/3.18 | | | | | | | | | | | | | | (294) ~ (all_250_1 = 0) | ~ (all_250_2 = 0) | % 16.93/3.18 | | | | | | | | | | | | | | all_250_0 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | DELTA: instantiating (280) with fresh symbols all_252_0, % 16.93/3.18 | | | | | | | | | | | | | | all_252_1, all_252_2 gives: % 16.93/3.18 | | | | | | | | | | | | | | (295) sdtasdt0(all_92_1, xp) = all_252_0 & % 16.93/3.18 | | | | | | | | | | | | | | aInteger0(all_92_1) = all_252_1 & aInteger0(xp) = % 16.93/3.18 | | | | | | | | | | | | | | all_252_2 & $i(all_252_0) & ( ~ (all_252_1 = 0) | % 16.93/3.18 | | | | | | | | | | | | | | ~ (all_252_2 = 0) | all_252_0 = all_22_1) % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | ALPHA: (295) implies: % 16.93/3.18 | | | | | | | | | | | | | | (296) aInteger0(xp) = all_252_2 % 16.93/3.18 | | | | | | | | | | | | | | (297) aInteger0(all_92_1) = all_252_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | DELTA: instantiating (283) with fresh symbols all_254_0, % 16.93/3.18 | | | | | | | | | | | | | | all_254_1, all_254_2 gives: % 16.93/3.18 | | | | | | | | | | | | | | (298) sdtasdt0(all_33_0, xq) = all_254_0 & % 16.93/3.18 | | | | | | | | | | | | | | aInteger0(all_33_0) = all_254_1 & aInteger0(xq) = % 16.93/3.18 | | | | | | | | | | | | | | all_254_2 & $i(all_254_0) & ( ~ (all_254_1 = 0) | % 16.93/3.18 | | | | | | | | | | | | | | ~ (all_254_2 = 0) | all_254_0 = all_92_1) % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | ALPHA: (298) implies: % 16.93/3.18 | | | | | | | | | | | | | | (299) aInteger0(xq) = all_254_2 % 16.93/3.18 | | | | | | | | | | | | | | (300) aInteger0(all_33_0) = all_254_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | DELTA: instantiating (282) with fresh symbols all_258_0, % 16.93/3.18 | | | | | | | | | | | | | | all_258_1, all_258_2, all_258_3, all_258_4 gives: % 16.93/3.18 | | | | | | | | | | | | | | (301) sdtasdt0(xq, all_258_1) = all_258_0 & sdtasdt0(xp, % 16.93/3.18 | | | | | | | | | | | | | | all_33_0) = all_258_1 & aInteger0(all_33_0) = % 16.93/3.18 | | | | | | | | | | | | | | all_258_2 & aInteger0(xq) = all_258_4 & % 16.93/3.18 | | | | | | | | | | | | | | aInteger0(xp) = all_258_3 & $i(all_258_0) & % 16.93/3.18 | | | | | | | | | | | | | | $i(all_258_1) & ( ~ (all_258_2 = 0) | ~ % 16.93/3.18 | | | | | | | | | | | | | | (all_258_3 = 0) | ~ (all_258_4 = 0) | all_258_0 % 16.93/3.18 | | | | | | | | | | | | | | = all_22_1) % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | ALPHA: (301) implies: % 16.93/3.18 | | | | | | | | | | | | | | (302) aInteger0(xp) = all_258_3 % 16.93/3.18 | | | | | | | | | | | | | | (303) aInteger0(xq) = all_258_4 % 16.93/3.18 | | | | | | | | | | | | | | (304) aInteger0(all_33_0) = all_258_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_258_3, xp, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (4), (302) gives: % 16.93/3.18 | | | | | | | | | | | | | | (305) all_258_3 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_252_2, all_258_3, xp, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (296), (302) gives: % 16.93/3.18 | | | | | | | | | | | | | | (306) all_258_3 = all_252_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_248_2, all_258_3, xp, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (288), (302) gives: % 16.93/3.18 | | | | | | | | | | | | | | (307) all_258_3 = all_248_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_258_4, xq, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (5), (303) gives: % 16.93/3.18 | | | | | | | | | | | | | | (308) all_258_4 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_254_2, all_258_4, xq, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (299), (303) gives: % 16.93/3.18 | | | | | | | | | | | | | | (309) all_258_4 = all_254_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_250_2, all_258_4, xq, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (291), (303) gives: % 16.93/3.18 | | | | | | | | | | | | | | (310) all_258_4 = all_250_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_254_1, all_33_0, % 16.93/3.18 | | | | | | | | | | | | | | simplifying with (48), (300) gives: % 16.93/3.18 | | | | | | | | | | | | | | (311) all_254_1 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_254_1, all_258_2, % 16.93/3.18 | | | | | | | | | | | | | | all_33_0, simplifying with (300), (304) gives: % 16.93/3.18 | | | | | | | | | | | | | | (312) all_258_2 = all_254_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_250_1, all_258_2, % 16.93/3.18 | | | | | | | | | | | | | | all_33_0, simplifying with (292), (304) gives: % 16.93/3.18 | | | | | | | | | | | | | | (313) all_258_2 = all_250_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_250_0, all_252_1, % 16.93/3.18 | | | | | | | | | | | | | | all_92_1, simplifying with (293), (297) gives: % 16.93/3.18 | | | | | | | | | | | | | | (314) all_252_1 = all_250_0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_248_1, all_252_1, % 16.93/3.18 | | | | | | | | | | | | | | all_92_1, simplifying with (289), (297) gives: % 16.93/3.18 | | | | | | | | | | | | | | (315) all_252_1 = all_248_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (312), (313) imply: % 16.93/3.18 | | | | | | | | | | | | | | (316) all_254_1 = all_250_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | SIMP: (316) implies: % 16.93/3.18 | | | | | | | | | | | | | | (317) all_254_1 = all_250_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (305), (306) imply: % 16.93/3.18 | | | | | | | | | | | | | | (318) all_252_2 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (306), (307) imply: % 16.93/3.18 | | | | | | | | | | | | | | (319) all_252_2 = all_248_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (308), (309) imply: % 16.93/3.18 | | | | | | | | | | | | | | (320) all_254_2 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (309), (310) imply: % 16.93/3.18 | | | | | | | | | | | | | | (321) all_254_2 = all_250_2 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (311), (317) imply: % 16.93/3.18 | | | | | | | | | | | | | | (322) all_250_1 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (320), (321) imply: % 16.93/3.18 | | | | | | | | | | | | | | (323) all_250_2 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (314), (315) imply: % 16.93/3.18 | | | | | | | | | | | | | | (324) all_250_0 = all_248_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | SIMP: (324) implies: % 16.93/3.18 | | | | | | | | | | | | | | (325) all_250_0 = all_248_1 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | COMBINE_EQS: (318), (319) imply: % 16.93/3.18 | | | | | | | | | | | | | | (326) all_248_2 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | SIMP: (326) implies: % 16.93/3.18 | | | | | | | | | | | | | | (327) all_248_2 = 0 % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | BETA: splitting (294) gives: % 16.93/3.18 | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | Case 1: % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | (328) ~ (all_250_1 = 0) % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | REDUCE: (322), (328) imply: % 16.93/3.18 | | | | | | | | | | | | | | | (329) $false % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | CLOSE: (329) is inconsistent. % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | Case 2: % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | (330) ~ (all_250_2 = 0) | all_250_0 = 0 % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | BETA: splitting (330) gives: % 16.93/3.18 | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | Case 1: % 16.93/3.18 | | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | | (331) ~ (all_250_2 = 0) % 16.93/3.18 | | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | | REDUCE: (323), (331) imply: % 16.93/3.18 | | | | | | | | | | | | | | | | (332) $false % 16.93/3.18 | | | | | | | | | | | | | | | | % 16.93/3.18 | | | | | | | | | | | | | | | | CLOSE: (332) is inconsistent. % 16.93/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | Case 2: % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | (333) all_250_0 = 0 % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | COMBINE_EQS: (325), (333) imply: % 17.28/3.18 | | | | | | | | | | | | | | | | (334) all_248_1 = 0 % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | SIMP: (334) implies: % 17.28/3.18 | | | | | | | | | | | | | | | | (335) all_248_1 = 0 % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | REDUCE: (289), (335) imply: % 17.28/3.18 | | | | | | | | | | | | | | | | (336) aInteger0(all_92_1) = 0 % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | BETA: splitting (45) gives: % 17.28/3.18 | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | Case 1: % 17.28/3.18 | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | (337) ~ (all_31_0 = 0) & ~ (all_31_1 = 0) & ! [v0: % 17.28/3.18 | | | | | | | | | | | | | | | | | $i] : ( ~ (sdtasdt0(xq, v0) = all_31_4) | ~ % 17.28/3.18 | | | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.18 | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.18 | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | ALPHA: (337) implies: % 17.28/3.18 | | | | | | | | | | | | | | | | | (338) ~ (all_31_1 = 0) % 17.28/3.18 | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | BETA: splitting (286) gives: % 17.28/3.18 | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | (339) xq = sz00 % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | REDUCE: (3), (339) imply: % 17.28/3.18 | | | | | | | | | | | | | | | | | | (340) $false % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | CLOSE: (340) is inconsistent. % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | (341) all_31_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 17.28/3.18 | | | | | | | | | | | | | | | | | | aInteger0(xq) = v0) | ! [v0: $i] : ( ~ % 17.28/3.18 | | | | | | | | | | | | | | | | | | (sdtasdt0(xq, v0) = all_22_1) | ~ $i(v0) | ? % 17.28/3.18 | | | | | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1)) % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | BETA: splitting (341) gives: % 17.28/3.18 | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.18 | | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | | (342) all_31_1 = 0 % 17.28/3.18 | | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | | REDUCE: (338), (342) imply: % 17.28/3.18 | | | | | | | | | | | | | | | | | | | (343) $false % 17.28/3.18 | | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | | CLOSE: (343) is inconsistent. % 17.28/3.18 | | | | | | | | | | | | | | | | | | | % 17.28/3.18 | | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.18 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | (344) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(xq) = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ! [v0: $i] : ( ~ (sdtasdt0(xq, v0) = all_22_1) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | BETA: splitting (344) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (345) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(xq) = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (345) with fresh symbol all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (346) ~ (all_318_0 = 0) & aInteger0(xq) = all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ALPHA: (346) implies: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (347) ~ (all_318_0 = 0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (348) aInteger0(xq) = all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_318_0, xq, % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | simplifying with (5), (348) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (349) all_318_0 = 0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | REDUCE: (347), (349) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (350) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | CLOSE: (350) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (351) ! [v0: $i] : ( ~ (sdtasdt0(xq, v0) = all_22_1) | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (351) with all_24_0, simplifying % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | with (27), (73) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (352) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(all_24_0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (352) with fresh symbol all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (353) ~ (all_319_0 = 0) & aInteger0(all_24_0) = % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ALPHA: (353) implies: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (354) ~ (all_319_0 = 0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (355) aInteger0(all_24_0) = all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_319_0, all_24_0, % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | simplifying with (266), (355) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (356) all_319_0 = 0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | REDUCE: (354), (356) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (357) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | CLOSE: (357) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | Case 2: % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | (358) ~ (all_31_2 = 0) & ~ (all_31_3 = 0) & ! [v0: % 17.28/3.19 | | | | | | | | | | | | | | | | | $i] : ( ~ (sdtasdt0(xp, v0) = all_31_4) | ~ % 17.28/3.19 | | | | | | | | | | | | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | ALPHA: (358) implies: % 17.28/3.19 | | | | | | | | | | | | | | | | | (359) ~ (all_31_3 = 0) % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | BETA: splitting (285) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | (360) xp = sz00 % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | REDUCE: (2), (360) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | (361) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | CLOSE: (361) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | (362) all_31_3 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | | aInteger0(xp) = v0) | ! [v0: $i] : ( ~ % 17.28/3.19 | | | | | | | | | | | | | | | | | | (sdtasdt0(xp, v0) = all_22_1) | ~ $i(v0) | ? % 17.28/3.19 | | | | | | | | | | | | | | | | | | [v1: int] : ( ~ (v1 = 0) & aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | BETA: splitting (362) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | (363) all_31_3 = 0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | REDUCE: (359), (363) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | (364) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | CLOSE: (364) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | (365) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(xp) = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = all_22_1) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | BETA: splitting (365) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | Case 1: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (366) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(xp) = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (366) with fresh symbol all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (367) ~ (all_318_0 = 0) & aInteger0(xp) = all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ALPHA: (367) implies: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (368) ~ (all_318_0 = 0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (369) aInteger0(xp) = all_318_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_318_0, xp, % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | simplifying with (4), (369) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (370) all_318_0 = 0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | REDUCE: (368), (370) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (371) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | CLOSE: (371) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | Case 2: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (372) ! [v0: $i] : ( ~ (sdtasdt0(xp, v0) = all_22_1) | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | aInteger0(v0) = v1)) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (372) with all_92_1, simplifying % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | with (143), (270) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (373) ? [v0: int] : ( ~ (v0 = 0) & aInteger0(all_92_1) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | = v0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (373) with fresh symbol all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (374) ~ (all_319_0 = 0) & aInteger0(all_92_1) = % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | ALPHA: (374) implies: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (375) ~ (all_319_0 = 0) % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (376) aInteger0(all_92_1) = all_319_0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with 0, all_319_0, all_92_1, % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | simplifying with (336), (376) gives: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (377) all_319_0 = 0 % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | REDUCE: (375), (377) imply: % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | (378) $false % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | CLOSE: (378) is inconsistent. % 17.28/3.19 | | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | | % 17.28/3.19 | | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | | % 17.28/3.19 | | | | | | | | | End of split % 17.28/3.19 | | | | | | | | | % 17.28/3.19 | | | | | | | | End of split % 17.28/3.19 | | | | | | | | % 17.28/3.19 | | | | | | | End of split % 17.28/3.19 | | | | | | | % 17.28/3.19 | | | | | | End of split % 17.28/3.19 | | | | | | % 17.28/3.19 | | | | | End of split % 17.28/3.19 | | | | | % 17.28/3.19 | | | | End of split % 17.28/3.19 | | | | % 17.28/3.19 | | | End of split % 17.28/3.19 | | | % 17.28/3.19 | | End of split % 17.28/3.19 | | % 17.28/3.19 | End of split % 17.28/3.19 | % 17.28/3.19 End of proof % 17.28/3.19 % SZS output end Proof for theBenchmark % 17.28/3.19 % 17.28/3.19 2598ms %------------------------------------------------------------------------------