%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV469+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n020.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 22:56:37 EDT 2023 % Result : Theorem 75.57s 10.57s % Output : Proof 78.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV469+1 : TPTP v8.1.2. Released v4.0.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Aug 29 04:17:13 EDT 2023 % 0.12/0.34 % CPUTime : % 0.64/0.63 ________ _____ % 0.64/0.63 ___ __ \_________(_)________________________________ % 0.64/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.64/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.64/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.64/0.63 % 0.64/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.64/0.63 (2023-06-19) % 0.64/0.63 % 0.64/0.63 (c) Philipp Rümmer, 2009-2023 % 0.64/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.64/0.63 Amanda Stjerna. % 0.64/0.63 Free software under BSD-3-Clause. % 0.64/0.63 % 0.64/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.64/0.63 % 0.64/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.64/0.65 Running up to 7 provers in parallel. % 0.64/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.64/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.64/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.64/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.64/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.64/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.64/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.68/1.27 Prover 1: Preprocessing ... % 3.68/1.28 Prover 4: Preprocessing ... % 4.38/1.32 Prover 5: Preprocessing ... % 4.38/1.32 Prover 0: Preprocessing ... % 4.38/1.32 Prover 3: Preprocessing ... % 4.38/1.32 Prover 2: Preprocessing ... % 4.38/1.32 Prover 6: Preprocessing ... % 12.09/2.34 Prover 3: Constructing countermodel ... % 12.09/2.34 Prover 1: Constructing countermodel ... % 12.09/2.36 Prover 6: Proving ... % 12.76/2.48 Prover 5: Proving ... % 12.76/2.53 Prover 2: Proving ... % 16.42/2.90 Prover 0: Proving ... % 16.42/2.94 Prover 4: Constructing countermodel ... % 17.68/3.16 Prover 3: gave up % 17.68/3.16 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.62/3.24 Prover 7: Preprocessing ... % 20.93/3.50 Prover 1: gave up % 20.93/3.51 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 21.54/3.57 Prover 8: Preprocessing ... % 22.94/3.80 Prover 8: Warning: ignoring some quantifiers % 23.61/3.86 Prover 8: Constructing countermodel ... % 24.36/3.93 Prover 7: Warning: ignoring some quantifiers % 24.36/3.95 Prover 7: Constructing countermodel ... % 31.65/4.87 Prover 8: gave up % 31.65/4.89 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 32.42/4.97 Prover 9: Preprocessing ... % 35.20/5.37 Prover 9: Constructing countermodel ... % 59.47/8.51 Prover 2: stopped % 60.03/8.53 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 60.43/8.61 Prover 10: Preprocessing ... % 61.06/8.72 Prover 10: Warning: ignoring some quantifiers % 61.58/8.74 Prover 10: Constructing countermodel ... % 75.57/10.57 Prover 9: proved (5684ms) % 75.57/10.57 % 75.57/10.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.57/10.57 % 75.57/10.57 Prover 5: stopped % 76.08/10.60 Prover 6: stopped % 76.08/10.60 Prover 0: stopped % 76.08/10.61 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 76.08/10.61 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 76.08/10.61 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 76.08/10.61 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 76.08/10.65 Prover 10: Found proof (size 166) % 76.08/10.65 Prover 10: proved (2115ms) % 76.08/10.66 Prover 11: Preprocessing ... % 76.08/10.66 Prover 19: Preprocessing ... % 76.08/10.66 Prover 7: stopped % 76.08/10.66 Prover 13: Preprocessing ... % 76.08/10.67 Prover 4: stopped % 76.08/10.68 Prover 16: Preprocessing ... % 76.90/10.70 Prover 11: stopped % 76.90/10.70 Prover 13: stopped % 76.90/10.71 Prover 16: stopped % 77.26/10.77 Prover 19: Warning: ignoring some quantifiers % 77.26/10.78 Prover 19: Constructing countermodel ... % 77.26/10.78 Prover 19: stopped % 77.26/10.78 % 77.26/10.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 77.26/10.78 % 77.26/10.79 % SZS output start Proof for theBenchmark % 77.26/10.80 Assumptions after simplification: % 77.26/10.80 --------------------------------- % 77.26/10.80 % 77.26/10.80 (axiom_01) % 77.48/10.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (host(v1) = v2) | ~ (host(v0) = % 77.48/10.82 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 = v2) & s(v2) = v3 & % 77.48/10.82 $i(v3))) % 77.48/10.82 % 77.48/10.82 (axiom_03) % 77.48/10.82 $i(nbr_proc) & $i(zero) & ? [v0: $i] : (s(zero) = v0 & $i(v0) & leq(v0, % 77.48/10.82 nbr_proc)) % 77.48/10.82 % 77.48/10.82 (axiom_17) % 77.48/10.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (m_Down(v0) = v2) | ~ % 77.48/10.82 (m_Halt(v1) = v2) | ~ $i(v1) | ~ $i(v0)) % 77.48/10.82 % 77.48/10.82 (axiom_30) % 77.48/10.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (m_Down(v1) = v2) | ~ % 77.48/10.83 (m_Down(v0) = v2) | ~ $i(v1) | ~ $i(v0)) % 77.48/10.83 % 77.48/10.83 (axiom_46) % 77.48/10.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 77.48/10.83 (cons(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v3) | % 77.48/10.83 elem(v0, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 77.48/10.83 (cons(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v2) | % 77.48/10.83 elem(v0, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (cons(v0, v1) % 77.48/10.83 = v2) | ~ $i(v1) | ~ $i(v0) | elem(v0, v2)) % 77.48/10.83 % 77.48/10.83 (axiom_48) % 77.48/10.83 ! [v0: $i] : ! [v1: $i] : ( ~ (m_Down(v1) = v0) | ~ $i(v1) | ~ $i(v0) | % 77.48/10.83 pidElem(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (m_Halt(v1) = v0) | ~ $i(v1) % 77.48/10.83 | ~ $i(v0) | pidElem(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ pidElem(v0) | ? % 77.48/10.83 [v1: $i] : ? [v2: $i] : ? [v3: $i] : ($i(v1) & ((v3 = v0 & m_Down(v1) = % 77.48/10.83 v0) | (v2 = v0 & m_Halt(v1) = v0)))) % 77.48/10.83 % 77.48/10.83 (axiom_61) % 77.48/10.83 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ leq(v1, v0) % 77.48/10.83 | ~ leq(v0, v1)) & ? [v0: $i] : ( ~ $i(v0) | leq(v0, v0)) % 77.48/10.83 % 77.48/10.83 (axiom_63) % 77.48/10.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s(v1) = v3) | ~ % 77.48/10.83 (s(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v2, v3) | leq(v0, v1)) & ! % 77.48/10.83 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s(v1) = v3) | ~ % 77.48/10.83 (s(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v0, v1) | leq(v2, v3)) % 77.48/10.83 % 77.48/10.83 (axiom_64) % 77.48/10.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (s(v1) = v2) | ~ % 77.48/10.84 $i(v1) | ~ $i(v0) | ~ leq(v0, v2) | leq(v0, v1)) & ! [v0: $i] : ! [v1: % 77.48/10.84 $i] : ! [v2: $i] : ( ~ (s(v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v0, % 77.48/10.84 v1) | leq(v0, v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ (s(v1) = v0) | ~ % 77.48/10.84 $i(v1) | ~ $i(v0) | leq(v0, v0)) % 77.48/10.84 % 77.48/10.84 (conj) % 77.66/10.86 $i(ldr) & $i(pendack) & $i(down) & $i(elid) & $i(status) & $i(alive) & % 77.66/10.86 $i(norm) & $i(wait) & $i(elec_1) & $i(elec_2) & $i(nbr_proc) & $i(zero) & ? % 77.66/10.86 [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] % 77.66/10.86 : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? % 77.66/10.86 [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? % 77.66/10.86 [v16: $i] : ( ~ (v15 = v5) & index(ldr, v15) = v15 & index(down, v5) = v12 & % 77.66/10.86 index(status, v15) = norm & index(status, v5) = elec_1 & cons(v7, v1) = v6 & % 77.66/10.86 m_Down(v4) = v7 & s(v5) = v13 & s(zero) = v0 & host(v16) = v5 & host(v14) = % 77.66/10.86 v15 & host(v4) = v8 & host(v3) = v5 & queue(v5) = v6 & $i(v16) & $i(v15) & % 77.66/10.86 $i(v14) & $i(v13) & $i(v12) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 77.66/10.86 $i(v3) & $i(v2) & $i(v1) & $i(v0) & setIn(v16, alive) & setIn(v14, alive) & % 77.66/10.86 setIn(v3, alive) & ~ leq(v13, v15) & ~ leq(v5, v8) & ~ leq(nbr_proc, v5) % 77.66/10.86 & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 77.66/10.86 ! [v22: $i] : ( ~ (m_Down(v18) = v22) | ~ (host(v19) = v20) | ~ % 77.66/10.86 (host(v17) = v21) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, % 77.66/10.86 alive) | ~ setIn(v17, alive) | leq(v20, v21) | ? [v23: $i] : ? [v24: % 77.66/10.86 $i] : ? [v25: $i] : (( ~ (v24 = elec_2) & index(status, v20) = v24 & % 77.66/10.86 $i(v24)) | ( ~ (v23 = v20) & host(v18) = v23 & $i(v23)) | (queue(v21) % 77.66/10.86 = v25 & $i(v25) & ~ elem(v22, v25)))) & ! [v17: $i] : ! [v18: $i] : % 77.66/10.86 ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Down(v18) % 77.66/10.86 = v22) | ~ (host(v19) = v20) | ~ (host(v17) = v21) | ~ $i(v19) | ~ % 77.66/10.86 $i(v18) | ~ $i(v17) | ~ setIn(v17, alive) | leq(v20, v21) | ? [v23: $i] % 77.66/10.86 : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] % 77.66/10.86 : ? [v29: $i] : ($i(v29) & (( ~ (v29 = v24) & index(down, v20) = v23 & % 77.66/10.86 host(v18) = v24 & $i(v24) & $i(v23) & leq(v0, v29) & ~ leq(v20, % 77.66/10.86 v29) & ~ setIn(v29, v23)) | ( ~ (v28 = norm) & index(status, v21) % 77.66/10.86 = v28 & $i(v28)) | ( ~ (v27 = v21) & index(ldr, v21) = v27 & % 77.66/10.86 $i(v27)) | ( ~ (v26 = elec_1) & index(status, v20) = v26 & $i(v26)) % 77.66/10.86 | (queue(v20) = v25 & $i(v25) & ~ elem(v22, v25))))) & ! [v17: $i] : % 77.66/10.86 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( % 77.66/10.86 ~ (m_Down(v18) = v21) | ~ (host(v19) = v20) | ~ (host(v17) = v22) | ~ % 77.66/10.86 $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, % 77.66/10.86 alive) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : (( % 77.66/10.86 ~ (v25 = v20) & index(ldr, v20) = v25 & $i(v25)) | ( ~ (v24 = norm) & % 77.66/10.86 index(status, v20) = v24 & $i(v24)) | ( ~ (v23 = v20) & host(v18) = % 77.66/10.86 v23 & $i(v23)) | (queue(v22) = v26 & $i(v26) & ~ elem(v21, v26)))) & % 77.66/10.86 ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! % 77.66/10.86 [v22: $i] : ( ~ (m_Down(v18) = v20) | ~ (host(v19) = v22) | ~ (host(v17) = % 77.66/10.86 v21) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ % 77.66/10.86 setIn(v17, alive) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: % 77.66/10.86 $i] : (( ~ (v25 = elec_2) & index(status, v22) = v25 & $i(v25)) | ( ~ % 77.66/10.86 (v24 = v22) & host(v18) = v24 & $i(v24)) | (index(pendack, v22) = v26 % 77.66/10.86 & $i(v26) & leq(v26, v21)) | (queue(v21) = v23 & $i(v23) & ~ % 77.66/10.86 elem(v20, v23)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! % 77.66/10.86 [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Down(v18) = v20) | ~ % 77.66/10.86 (host(v19) = v21) | ~ (host(v17) = v22) | ~ $i(v19) | ~ $i(v18) | ~ % 77.66/10.86 $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, alive) | ? [v23: $i] : ? % 77.66/10.86 [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : (( ~ (v27 = norm) % 77.66/10.86 & index(status, v22) = v27 & $i(v27)) | ( ~ (v26 = v22) & index(ldr, % 77.66/10.86 v22) = v26 & $i(v26)) | ( ~ (v25 = elec_2) & index(status, v21) = % 77.66/10.86 v25 & $i(v25)) | ( ~ (v24 = v22) & host(v18) = v24 & $i(v24)) | % 77.66/10.86 (queue(v21) = v23 & $i(v23) & ~ elem(v20, v23)))) & ! [v17: $i] : ! % 77.66/10.86 [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ (m_Ack(v19, % 77.66/10.86 v18) = v20) | ~ (host(v17) = v21) | ~ $i(v19) | ~ $i(v18) | ~ % 77.66/10.86 $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, alive) | ? [v22: $i] : ? % 77.66/10.86 [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : (( ~ (v26 = norm) % 77.66/10.86 & index(status, v21) = v26 & $i(v26)) | ( ~ (v25 = v21) & index(ldr, % 77.66/10.86 v21) = v25 & $i(v25)) | ( ~ (v24 = v21) & host(v18) = v24 & $i(v24)) % 77.66/10.86 | (host(v19) = v22 & queue(v22) = v23 & $i(v23) & $i(v22) & ~ elem(v20, % 77.66/10.86 v23)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] % 77.66/10.86 : ! [v21: $i] : ( ~ (m_Ack(v17, v18) = v21) | ~ (host(v19) = v20) | ~ % 77.66/10.86 $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, % 77.66/10.86 alive) | ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? % 77.66/10.86 [v26: $i] : (( ~ (v25 = elec_2) & index(status, v20) = v25 & $i(v25)) | ( % 77.66/10.86 ~ (v24 = elec_2) & index(status, v23) = v24 & host(v17) = v23 & % 77.66/10.86 $i(v24) & $i(v23)) | ( ~ (v22 = v20) & host(v18) = v22 & $i(v22)) | % 77.66/10.86 (host(v17) = v23 & queue(v23) = v26 & $i(v26) & $i(v23) & ~ elem(v21, % 77.66/10.86 v26)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] % 77.66/10.86 : ( ~ (m_Ldr(v18) = v19) | ~ (host(v17) = v20) | ~ $i(v18) | ~ $i(v17) | % 77.66/10.86 ? [v21: $i] : ? [v22: $i] : ((host(v18) = v22 & $i(v22) & ~ leq(v20, % 77.66/10.86 v22)) | (queue(v20) = v21 & $i(v21) & ~ elem(v19, v21)))) & ! % 77.66/10.86 [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = % 77.66/10.86 v20) | ~ (host(v17) = v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, % 77.66/10.86 alive) | ~ setIn(v17, alive) | leq(v19, v20) | ? [v21: $i] : ? [v22: % 77.66/10.86 $i] : ? [v23: $i] : ? [v24: $i] : (( ~ (v22 = elec_2) & index(status, % 77.66/10.86 v20) = v22 & $i(v22)) | ( ~ (v21 = elec_2) & index(status, v19) = % 77.66/10.86 v21 & $i(v21)) | (index(pendack, v20) = v24 & index(pendack, v19) = % 77.66/10.86 v23 & $i(v24) & $i(v23) & ~ leq(v23, v24)))) & ! [v17: $i] : ! % 77.66/10.86 [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = v20) | ~ % 77.66/10.86 (host(v17) = v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ % 77.66/10.86 setIn(v17, alive) | leq(v19, v20) | ? [v21: $i] : ? [v22: $i] : ? [v23: % 77.66/10.86 $i] : (( ~ (v22 = elec_2) & index(status, v20) = v22 & $i(v22)) | ( ~ % 77.66/10.86 (v21 = elec_2) & index(status, v19) = v21 & $i(v21)) | (index(pendack, % 77.66/10.86 v20) = v23 & $i(v23) & leq(v23, v19)))) & ! [v17: $i] : ! [v18: % 77.66/10.86 $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = v19) | ~ (host(v17) % 77.66/10.86 = v20) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ setIn(v17, % 77.66/10.86 alive) | ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : (( % 77.66/10.86 ~ (v24 = norm) & index(status, v20) = v24 & $i(v24)) | ( ~ (v23 = v20) % 77.66/10.86 & index(ldr, v20) = v23 & $i(v23)) | ( ~ (v22 = elec_2) & % 77.66/10.86 index(status, v19) = v22 & $i(v22)) | (index(pendack, v19) = v21 & % 77.66/10.86 $i(v21) & leq(v21, v20)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: % 77.66/10.86 $i] : ! [v20: $i] : ( ~ (host(v18) = v19) | ~ (host(v17) = v20) | ~ % 77.66/10.86 $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ setIn(v17, alive) | ? % 77.66/10.86 [v21: $i] : ? [v22: $i] : ? [v23: $i] : (( ~ (v22 = v19) & index(ldr, % 77.66/10.86 v19) = v22 & $i(v22)) | ( ~ (v21 = norm) & index(status, v19) = v21 % 77.66/10.86 & $i(v21)) | (index(down, v20) = v23 & $i(v23) & ~ setIn(v19, v23)))) % 77.66/10.86 & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) % 77.66/10.86 = v19) | ~ (host(v17) = v20) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, % 77.66/10.86 alive) | ~ setIn(v17, alive) | ? [v21: $i] : ? [v22: $i] : ? [v23: % 77.66/10.86 $i] : (( ~ (v22 = elec_2) & index(status, v19) = v22 & $i(v22)) | % 77.66/10.86 (index(pendack, v19) = v23 & $i(v23) & leq(v23, v20)) | (index(down, % 77.66/10.86 v20) = v21 & $i(v21) & ~ setIn(v19, v21)))) & ! [v17: $i] : ! % 77.66/10.86 [v18: $i] : ! [v19: $i] : (v18 = v17 | ~ (host(v18) = v19) | ~ (host(v17) % 77.66/10.86 = v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ setIn(v17, % 77.66/10.86 alive)) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ( ~ (m_Ack(v17, % 77.66/10.86 v18) = v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ? % 77.66/10.86 [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : (( ~ (v21 = % 77.66/10.86 elec_2) & index(status, v20) = v21 & host(v18) = v20 & $i(v21) & % 77.66/10.86 $i(v20)) | (host(v17) = v22 & queue(v22) = v23 & $i(v23) & $i(v22) & % 77.66/10.86 ~ elem(v19, v23)))) & ! [v17: $i] : ! [v18: $i] : ( ~ (host(v17) = % 77.66/10.86 v18) | ~ $i(v17) | ~ setIn(v17, alive) | ? [v19: $i] : ? [v20: $i] : % 77.66/10.86 ((v20 = v17 & index(elid, v18) = v17) | ( ~ (v19 = elec_1) & ~ (v19 = % 77.66/10.86 elec_2) & index(status, v18) = v19 & $i(v19)))) & ! [v17: $i] : % 77.66/10.86 (v17 = v8 | ~ $i(v17) | ~ leq(v0, v17) | leq(v5, v17) | setIn(v17, v12)) & % 77.66/10.86 ( ~ (norm = elec_1) | ( ~ (v9 = v8) & index(ldr, v5) = v9 & $i(v9))) & ( ~ % 77.66/10.86 (wait = elec_1) | ( ~ (v11 = v8) & index(elid, v5) = v10 & host(v10) = v11 % 77.66/10.86 & $i(v11) & $i(v10)))) % 77.66/10.86 % 77.66/10.86 (function-axioms) % 77.66/10.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 77.66/10.87 (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 77.66/10.87 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (snoc(v3, v2) = v1) | ~ (snoc(v3, % 77.66/10.87 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 77.66/10.87 = v0 | ~ (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) & ! [v0: $i] : ! % 77.66/10.87 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (m_Ack(v3, v2) = v1) | ~ % 77.66/10.87 (m_Ack(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 77.66/10.87 ~ (pidMsg(v2) = v1) | ~ (pidMsg(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 77.66/10.87 ! [v2: $i] : (v1 = v0 | ~ (init(v2) = v1) | ~ (init(v2) = v0)) & ! [v0: $i] % 77.66/10.87 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (last(v2) = v1) | ~ (last(v2) = % 77.66/10.87 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (tail(v2) = % 77.66/10.87 v1) | ~ (tail(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 77.66/10.87 = v0 | ~ (head(v2) = v1) | ~ (head(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 77.66/10.87 : ! [v2: $i] : (v1 = v0 | ~ (m_NormQ(v2) = v1) | ~ (m_NormQ(v2) = v0)) & ! % 77.66/10.87 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (m_Ldr(v2) = v1) | ~ % 77.66/10.87 (m_Ldr(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 77.66/10.87 (m_NotNorm(v2) = v1) | ~ (m_NotNorm(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 77.66/10.87 : ! [v2: $i] : (v1 = v0 | ~ (m_Down(v2) = v1) | ~ (m_Down(v2) = v0)) & ! % 77.66/10.87 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (m_Halt(v2) = v1) | ~ % 77.66/10.87 (m_Halt(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 77.66/10.87 (s(v2) = v1) | ~ (s(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 77.66/10.87 (v1 = v0 | ~ (host(v2) = v1) | ~ (host(v2) = v0)) & ! [v0: $i] : ! [v1: % 77.66/10.87 $i] : ! [v2: $i] : (v1 = v0 | ~ (queue(v2) = v1) | ~ (queue(v2) = v0)) % 77.66/10.87 % 77.66/10.87 Further assumptions not needed in the proof: % 77.66/10.87 -------------------------------------------- % 77.66/10.87 axiom, axiom_02, axiom_04, axiom_05, axiom_06, axiom_07, axiom_08, axiom_09, % 77.66/10.87 axiom_10, axiom_11, axiom_12, axiom_13, axiom_14, axiom_15, axiom_16, axiom_18, % 77.66/10.87 axiom_19, axiom_20, axiom_21, axiom_22, axiom_23, axiom_24, axiom_25, axiom_26, % 77.66/10.87 axiom_27, axiom_28, axiom_29, axiom_31, axiom_32, axiom_33, axiom_34, axiom_35, % 77.66/10.87 axiom_36, axiom_37, axiom_38, axiom_39, axiom_40, axiom_41, axiom_42, axiom_43, % 77.66/10.87 axiom_44, axiom_45, axiom_47, axiom_49, axiom_50, axiom_51, axiom_52, axiom_53, % 77.66/10.87 axiom_54, axiom_55, axiom_56, axiom_57, axiom_58, axiom_59, axiom_60, axiom_62, % 77.66/10.87 axiom_65 % 77.66/10.87 % 77.66/10.87 Those formulas are unsatisfiable: % 77.66/10.87 --------------------------------- % 77.66/10.87 % 77.66/10.87 Begin of proof % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_03) implies: % 77.66/10.87 | (1) ? [v0: $i] : (s(zero) = v0 & $i(v0) & leq(v0, nbr_proc)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_46) implies: % 77.66/10.87 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (cons(v0, v1) = v2) | ~ % 77.66/10.87 | $i(v1) | ~ $i(v0) | elem(v0, v2)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_48) implies: % 77.66/10.87 | (3) ! [v0: $i] : ( ~ $i(v0) | ~ pidElem(v0) | ? [v1: $i] : ? [v2: $i] : % 77.66/10.87 | ? [v3: $i] : ($i(v1) & ((v3 = v0 & m_Down(v1) = v0) | (v2 = v0 & % 77.66/10.87 | m_Halt(v1) = v0)))) % 77.66/10.87 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (m_Down(v1) = v0) | ~ $i(v1) | ~ % 77.66/10.87 | $i(v0) | pidElem(v0)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_61) implies: % 77.66/10.87 | (5) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 77.66/10.87 | leq(v1, v0) | ~ leq(v0, v1)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_63) implies: % 77.66/10.87 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s(v1) = % 77.66/10.87 | v3) | ~ (s(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v0, v1) | % 77.66/10.87 | leq(v2, v3)) % 77.66/10.87 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s(v1) = % 77.66/10.87 | v3) | ~ (s(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v2, v3) | % 77.66/10.87 | leq(v0, v1)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (axiom_64) implies: % 77.66/10.87 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (s(v1) = v2) | % 77.66/10.87 | ~ $i(v1) | ~ $i(v0) | ~ leq(v0, v2) | leq(v0, v1)) % 77.66/10.87 | % 77.66/10.87 | ALPHA: (conj) implies: % 77.66/10.89 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 77.66/10.89 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 77.66/10.89 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 77.66/10.89 | ? [v15: $i] : ? [v16: $i] : ( ~ (v15 = v5) & index(ldr, v15) = v15 & % 77.66/10.89 | index(down, v5) = v12 & index(status, v15) = norm & index(status, v5) % 77.66/10.89 | = elec_1 & cons(v7, v1) = v6 & m_Down(v4) = v7 & s(v5) = v13 & % 77.66/10.89 | s(zero) = v0 & host(v16) = v5 & host(v14) = v15 & host(v4) = v8 & % 77.66/10.89 | host(v3) = v5 & queue(v5) = v6 & $i(v16) & $i(v15) & $i(v14) & % 77.66/10.89 | $i(v13) & $i(v12) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 77.66/10.89 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & setIn(v16, alive) & setIn(v14, % 77.66/10.89 | alive) & setIn(v3, alive) & ~ leq(v13, v15) & ~ leq(v5, v8) & ~ % 77.66/10.89 | leq(nbr_proc, v5) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! % 77.66/10.89 | [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Down(v18) = v22) | % 77.66/10.89 | ~ (host(v19) = v20) | ~ (host(v17) = v21) | ~ $i(v19) | ~ % 77.66/10.89 | $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, alive) % 77.66/10.89 | | leq(v20, v21) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : (( ~ % 77.66/10.89 | (v24 = elec_2) & index(status, v20) = v24 & $i(v24)) | ( ~ (v23 % 77.66/10.89 | = v20) & host(v18) = v23 & $i(v23)) | (queue(v21) = v25 & % 77.66/10.89 | $i(v25) & ~ elem(v22, v25)))) & ! [v17: $i] : ! [v18: $i] : % 77.66/10.89 | ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ % 77.66/10.89 | (m_Down(v18) = v22) | ~ (host(v19) = v20) | ~ (host(v17) = v21) | % 77.66/10.89 | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v17, alive) | % 77.66/10.89 | leq(v20, v21) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? % 77.66/10.89 | [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? [v29: $i] : ($i(v29) & % 77.66/10.89 | (( ~ (v29 = v24) & index(down, v20) = v23 & host(v18) = v24 & % 77.66/10.89 | $i(v24) & $i(v23) & leq(v0, v29) & ~ leq(v20, v29) & ~ % 77.66/10.89 | setIn(v29, v23)) | ( ~ (v28 = norm) & index(status, v21) = % 77.66/10.89 | v28 & $i(v28)) | ( ~ (v27 = v21) & index(ldr, v21) = v27 & % 77.66/10.89 | $i(v27)) | ( ~ (v26 = elec_1) & index(status, v20) = v26 & % 77.66/10.89 | $i(v26)) | (queue(v20) = v25 & $i(v25) & ~ elem(v22, % 77.66/10.89 | v25))))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! % 77.66/10.89 | [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Down(v18) = v21) | % 77.66/10.89 | ~ (host(v19) = v20) | ~ (host(v17) = v22) | ~ $i(v19) | ~ % 77.66/10.89 | $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, alive) % 77.66/10.89 | | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : (( ~ % 77.66/10.89 | (v25 = v20) & index(ldr, v20) = v25 & $i(v25)) | ( ~ (v24 = % 77.66/10.89 | norm) & index(status, v20) = v24 & $i(v24)) | ( ~ (v23 = v20) % 77.66/10.89 | & host(v18) = v23 & $i(v23)) | (queue(v22) = v26 & $i(v26) & ~ % 77.66/10.89 | elem(v21, v26)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] % 77.66/10.89 | : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Down(v18) = % 77.66/10.89 | v20) | ~ (host(v19) = v22) | ~ (host(v17) = v21) | ~ $i(v19) | % 77.66/10.89 | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, % 77.66/10.89 | alive) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: % 77.66/10.89 | $i] : (( ~ (v25 = elec_2) & index(status, v22) = v25 & $i(v25)) | % 77.66/10.89 | ( ~ (v24 = v22) & host(v18) = v24 & $i(v24)) | (index(pendack, % 77.66/10.89 | v22) = v26 & $i(v26) & leq(v26, v21)) | (queue(v21) = v23 & % 77.66/10.89 | $i(v23) & ~ elem(v20, v23)))) & ! [v17: $i] : ! [v18: $i] : % 77.66/10.89 | ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ % 77.66/10.89 | (m_Down(v18) = v20) | ~ (host(v19) = v21) | ~ (host(v17) = v22) | % 77.66/10.89 | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ % 77.66/10.89 | setIn(v17, alive) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? % 77.66/10.89 | [v26: $i] : ? [v27: $i] : (( ~ (v27 = norm) & index(status, v22) = % 77.66/10.89 | v27 & $i(v27)) | ( ~ (v26 = v22) & index(ldr, v22) = v26 & % 77.66/10.89 | $i(v26)) | ( ~ (v25 = elec_2) & index(status, v21) = v25 & % 77.66/10.89 | $i(v25)) | ( ~ (v24 = v22) & host(v18) = v24 & $i(v24)) | % 77.66/10.89 | (queue(v21) = v23 & $i(v23) & ~ elem(v20, v23)))) & ! [v17: $i] % 77.66/10.89 | : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ % 77.66/10.89 | (m_Ack(v19, v18) = v20) | ~ (host(v17) = v21) | ~ $i(v19) | ~ % 77.66/10.89 | $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ setIn(v17, alive) % 77.66/10.89 | | ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? % 77.66/10.89 | [v26: $i] : (( ~ (v26 = norm) & index(status, v21) = v26 & $i(v26)) % 77.66/10.89 | | ( ~ (v25 = v21) & index(ldr, v21) = v25 & $i(v25)) | ( ~ (v24 = % 77.66/10.89 | v21) & host(v18) = v24 & $i(v24)) | (host(v19) = v22 & % 77.66/10.89 | queue(v22) = v23 & $i(v23) & $i(v22) & ~ elem(v20, v23)))) & % 77.66/10.89 | ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: % 77.66/10.89 | $i] : ( ~ (m_Ack(v17, v18) = v21) | ~ (host(v19) = v20) | ~ % 77.66/10.89 | $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v19, alive) | ~ % 77.66/10.89 | setIn(v17, alive) | ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? % 77.66/10.89 | [v25: $i] : ? [v26: $i] : (( ~ (v25 = elec_2) & index(status, v20) % 77.66/10.89 | = v25 & $i(v25)) | ( ~ (v24 = elec_2) & index(status, v23) = % 77.66/10.89 | v24 & host(v17) = v23 & $i(v24) & $i(v23)) | ( ~ (v22 = v20) & % 77.66/10.89 | host(v18) = v22 & $i(v22)) | (host(v17) = v23 & queue(v23) = % 77.66/10.89 | v26 & $i(v26) & $i(v23) & ~ elem(v21, v26)))) & ! [v17: $i] : % 77.66/10.89 | ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (m_Ldr(v18) = v19) | % 77.66/10.89 | ~ (host(v17) = v20) | ~ $i(v18) | ~ $i(v17) | ? [v21: $i] : ? % 77.66/10.89 | [v22: $i] : ((host(v18) = v22 & $i(v22) & ~ leq(v20, v22)) | % 77.66/10.89 | (queue(v20) = v21 & $i(v21) & ~ elem(v19, v21)))) & ! [v17: $i] % 77.66/10.89 | : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = v20) % 77.66/10.89 | | ~ (host(v17) = v19) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, % 77.66/10.89 | alive) | ~ setIn(v17, alive) | leq(v19, v20) | ? [v21: $i] : ? % 77.66/10.89 | [v22: $i] : ? [v23: $i] : ? [v24: $i] : (( ~ (v22 = elec_2) & % 77.66/10.89 | index(status, v20) = v22 & $i(v22)) | ( ~ (v21 = elec_2) & % 77.66/10.89 | index(status, v19) = v21 & $i(v21)) | (index(pendack, v20) = % 77.66/10.89 | v24 & index(pendack, v19) = v23 & $i(v24) & $i(v23) & ~ % 77.66/10.89 | leq(v23, v24)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : % 77.66/10.89 | ! [v20: $i] : ( ~ (host(v18) = v20) | ~ (host(v17) = v19) | ~ % 77.66/10.89 | $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ setIn(v17, alive) % 77.66/10.89 | | leq(v19, v20) | ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : (( ~ % 77.66/10.89 | (v22 = elec_2) & index(status, v20) = v22 & $i(v22)) | ( ~ (v21 % 77.66/10.89 | = elec_2) & index(status, v19) = v21 & $i(v21)) | % 77.66/10.89 | (index(pendack, v20) = v23 & $i(v23) & leq(v23, v19)))) & ! % 77.66/10.89 | [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ % 77.66/10.89 | (host(v18) = v19) | ~ (host(v17) = v20) | ~ $i(v18) | ~ $i(v17) % 77.66/10.89 | | ~ setIn(v18, alive) | ~ setIn(v17, alive) | ? [v21: $i] : ? % 77.66/10.89 | [v22: $i] : ? [v23: $i] : ? [v24: $i] : (( ~ (v24 = norm) & % 77.66/10.89 | index(status, v20) = v24 & $i(v24)) | ( ~ (v23 = v20) & % 77.66/10.89 | index(ldr, v20) = v23 & $i(v23)) | ( ~ (v22 = elec_2) & % 77.66/10.89 | index(status, v19) = v22 & $i(v22)) | (index(pendack, v19) = % 77.66/10.89 | v21 & $i(v21) & leq(v21, v20)))) & ! [v17: $i] : ! [v18: $i] % 77.66/10.89 | : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = v19) | ~ (host(v17) % 77.66/10.89 | = v20) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ~ % 77.66/10.89 | setIn(v17, alive) | ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : (( % 77.66/10.89 | ~ (v22 = v19) & index(ldr, v19) = v22 & $i(v22)) | ( ~ (v21 = % 77.66/10.89 | norm) & index(status, v19) = v21 & $i(v21)) | (index(down, % 77.66/10.89 | v20) = v23 & $i(v23) & ~ setIn(v19, v23)))) & ! [v17: $i] : % 77.66/10.89 | ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (host(v18) = v19) | % 77.66/10.89 | ~ (host(v17) = v20) | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, % 77.66/10.89 | alive) | ~ setIn(v17, alive) | ? [v21: $i] : ? [v22: $i] : ? % 77.66/10.89 | [v23: $i] : (( ~ (v22 = elec_2) & index(status, v19) = v22 & % 77.66/10.89 | $i(v22)) | (index(pendack, v19) = v23 & $i(v23) & leq(v23, % 77.66/10.89 | v20)) | (index(down, v20) = v21 & $i(v21) & ~ setIn(v19, % 77.66/10.89 | v21)))) & ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : (v18 = % 77.66/10.89 | v17 | ~ (host(v18) = v19) | ~ (host(v17) = v19) | ~ $i(v18) | ~ % 77.66/10.89 | $i(v17) | ~ setIn(v18, alive) | ~ setIn(v17, alive)) & ! [v17: % 77.66/10.89 | $i] : ! [v18: $i] : ! [v19: $i] : ( ~ (m_Ack(v17, v18) = v19) | % 77.66/10.89 | ~ $i(v18) | ~ $i(v17) | ~ setIn(v18, alive) | ? [v20: $i] : ? % 77.66/10.89 | [v21: $i] : ? [v22: $i] : ? [v23: $i] : (( ~ (v21 = elec_2) & % 77.66/10.89 | index(status, v20) = v21 & host(v18) = v20 & $i(v21) & $i(v20)) % 77.66/10.89 | | (host(v17) = v22 & queue(v22) = v23 & $i(v23) & $i(v22) & ~ % 77.66/10.89 | elem(v19, v23)))) & ! [v17: $i] : ! [v18: $i] : ( ~ % 77.66/10.89 | (host(v17) = v18) | ~ $i(v17) | ~ setIn(v17, alive) | ? [v19: % 77.66/10.89 | $i] : ? [v20: $i] : ((v20 = v17 & index(elid, v18) = v17) | ( ~ % 77.66/10.89 | (v19 = elec_1) & ~ (v19 = elec_2) & index(status, v18) = v19 & % 77.66/10.89 | $i(v19)))) & ! [v17: $i] : (v17 = v8 | ~ $i(v17) | ~ leq(v0, % 77.66/10.89 | v17) | leq(v5, v17) | setIn(v17, v12)) & ( ~ (norm = elec_1) | ( % 77.66/10.89 | ~ (v9 = v8) & index(ldr, v5) = v9 & $i(v9))) & ( ~ (wait = % 77.66/10.89 | elec_1) | ( ~ (v11 = v8) & index(elid, v5) = v10 & host(v10) = % 77.66/10.89 | v11 & $i(v11) & $i(v10)))) % 77.66/10.89 | % 77.66/10.89 | ALPHA: (function-axioms) implies: % 77.66/10.89 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (queue(v2) = % 77.66/10.89 | v1) | ~ (queue(v2) = v0)) % 77.66/10.89 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (host(v2) = % 77.66/10.89 | v1) | ~ (host(v2) = v0)) % 77.66/10.89 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | % 77.66/10.89 | ~ (s(v2) = v0)) % 77.66/10.89 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 77.66/10.89 | (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) % 77.66/10.89 | % 77.66/10.89 | DELTA: instantiating (1) with fresh symbol all_59_0 gives: % 77.66/10.89 | (14) s(zero) = all_59_0 & $i(all_59_0) & leq(all_59_0, nbr_proc) % 77.66/10.89 | % 77.66/10.89 | ALPHA: (14) implies: % 77.66/10.89 | (15) s(zero) = all_59_0 % 77.66/10.89 | % 77.66/10.89 | DELTA: instantiating (9) with fresh symbols all_65_0, all_65_1, all_65_2, % 77.66/10.89 | all_65_3, all_65_4, all_65_5, all_65_6, all_65_7, all_65_8, all_65_9, % 77.66/10.89 | all_65_10, all_65_11, all_65_12, all_65_13, all_65_14, all_65_15, % 77.66/10.89 | all_65_16 gives: % 77.66/10.91 | (16) ~ (all_65_1 = all_65_11) & index(ldr, all_65_1) = all_65_1 & % 77.66/10.91 | index(down, all_65_11) = all_65_4 & index(status, all_65_1) = norm & % 77.66/10.91 | index(status, all_65_11) = elec_1 & cons(all_65_9, all_65_15) = % 77.66/10.91 | all_65_10 & m_Down(all_65_12) = all_65_9 & s(all_65_11) = all_65_3 & % 77.66/10.91 | s(zero) = all_65_16 & host(all_65_0) = all_65_11 & host(all_65_2) = % 77.66/10.91 | all_65_1 & host(all_65_12) = all_65_8 & host(all_65_13) = all_65_11 & % 77.66/10.91 | queue(all_65_11) = all_65_10 & $i(all_65_0) & $i(all_65_1) & % 77.66/10.91 | $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & $i(all_65_8) & % 77.66/10.91 | $i(all_65_9) & $i(all_65_10) & $i(all_65_11) & $i(all_65_12) & % 77.66/10.91 | $i(all_65_13) & $i(all_65_14) & $i(all_65_15) & $i(all_65_16) & % 77.66/10.91 | setIn(all_65_0, alive) & setIn(all_65_2, alive) & setIn(all_65_13, % 77.66/10.91 | alive) & ~ leq(all_65_3, all_65_1) & ~ leq(all_65_11, all_65_8) & % 77.66/10.91 | ~ leq(nbr_proc, all_65_11) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 77.66/10.91 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (m_Down(v1) = v5) | ~ % 77.66/10.91 | (host(v2) = v3) | ~ (host(v0) = v4) | ~ $i(v2) | ~ $i(v1) | ~ % 77.66/10.91 | $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | leq(v3, v4) | % 77.66/10.91 | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (( ~ (v7 = elec_2) & % 77.66/10.91 | index(status, v3) = v7 & $i(v7)) | ( ~ (v6 = v3) & host(v1) = v6 % 77.66/10.91 | & $i(v6)) | (queue(v4) = v8 & $i(v8) & ~ elem(v5, v8)))) & ! % 77.66/10.91 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 77.66/10.91 | [v5: $i] : ( ~ (m_Down(v1) = v5) | ~ (host(v2) = v3) | ~ (host(v0) = % 77.66/10.91 | v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v0, alive) | % 77.66/10.91 | leq(v3, v4) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] % 77.66/10.91 | : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ($i(v12) & (( ~ (v12 % 77.66/10.91 | = v7) & index(down, v3) = v6 & host(v1) = v7 & $i(v7) & % 77.66/10.91 | $i(v6) & leq(all_65_16, v12) & ~ leq(v3, v12) & ~ setIn(v12, % 77.66/10.91 | v6)) | ( ~ (v11 = norm) & index(status, v4) = v11 & $i(v11)) % 77.66/10.91 | | ( ~ (v10 = v4) & index(ldr, v4) = v10 & $i(v10)) | ( ~ (v9 = % 77.66/10.91 | elec_1) & index(status, v3) = v9 & $i(v9)) | (queue(v3) = v8 % 77.66/10.91 | & $i(v8) & ~ elem(v5, v8))))) & ! [v0: $i] : ! [v1: $i] : % 77.66/10.91 | ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (m_Down(v1) % 77.66/10.91 | = v4) | ~ (host(v2) = v3) | ~ (host(v0) = v5) | ~ $i(v2) | ~ % 77.66/10.91 | $i(v1) | ~ $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? % 77.66/10.91 | [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : (( ~ (v8 = v3) % 77.66/10.91 | & index(ldr, v3) = v8 & $i(v8)) | ( ~ (v7 = norm) & % 77.66/10.91 | index(status, v3) = v7 & $i(v7)) | ( ~ (v6 = v3) & host(v1) = v6 % 77.66/10.91 | & $i(v6)) | (queue(v5) = v9 & $i(v9) & ~ elem(v4, v9)))) & ! % 77.66/10.91 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 77.66/10.91 | [v5: $i] : ( ~ (m_Down(v1) = v3) | ~ (host(v2) = v5) | ~ (host(v0) = % 77.66/10.91 | v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v2, alive) | ~ % 77.66/10.91 | setIn(v0, alive) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: % 77.66/10.91 | $i] : (( ~ (v8 = elec_2) & index(status, v5) = v8 & $i(v8)) | ( ~ % 77.66/10.91 | (v7 = v5) & host(v1) = v7 & $i(v7)) | (index(pendack, v5) = v9 & % 77.66/10.91 | $i(v9) & leq(v9, v4)) | (queue(v4) = v6 & $i(v6) & ~ elem(v3, % 77.66/10.91 | v6)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 77.66/10.91 | : ! [v4: $i] : ! [v5: $i] : ( ~ (m_Down(v1) = v3) | ~ (host(v2) = % 77.66/10.91 | v4) | ~ (host(v0) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 77.66/10.91 | setIn(v2, alive) | ~ setIn(v0, alive) | ? [v6: $i] : ? [v7: $i] : % 77.66/10.91 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : (( ~ (v10 = norm) & % 77.66/10.91 | index(status, v5) = v10 & $i(v10)) | ( ~ (v9 = v5) & index(ldr, % 77.66/10.91 | v5) = v9 & $i(v9)) | ( ~ (v8 = elec_2) & index(status, v4) = % 77.66/10.91 | v8 & $i(v8)) | ( ~ (v7 = v5) & host(v1) = v7 & $i(v7)) | % 77.66/10.91 | (queue(v4) = v6 & $i(v6) & ~ elem(v3, v6)))) & ! [v0: $i] : ! % 77.66/10.91 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (m_Ack(v2, % 77.66/10.91 | v1) = v3) | ~ (host(v0) = v4) | ~ $i(v2) | ~ $i(v1) | ~ % 77.66/10.91 | $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v5: $i] : % 77.66/10.91 | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : (( ~ (v9 = % 77.66/10.91 | norm) & index(status, v4) = v9 & $i(v9)) | ( ~ (v8 = v4) & % 77.66/10.91 | index(ldr, v4) = v8 & $i(v8)) | ( ~ (v7 = v4) & host(v1) = v7 & % 77.66/10.91 | $i(v7)) | (host(v2) = v5 & queue(v5) = v6 & $i(v6) & $i(v5) & ~ % 77.66/10.91 | elem(v3, v6)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 77.66/10.91 | [v3: $i] : ! [v4: $i] : ( ~ (m_Ack(v0, v1) = v4) | ~ (host(v2) = v3) % 77.66/10.91 | | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v2, alive) | ~ % 77.66/10.91 | setIn(v0, alive) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: % 77.66/10.91 | $i] : ? [v9: $i] : (( ~ (v8 = elec_2) & index(status, v3) = v8 & % 77.66/10.91 | $i(v8)) | ( ~ (v7 = elec_2) & index(status, v6) = v7 & host(v0) % 77.66/10.91 | = v6 & $i(v7) & $i(v6)) | ( ~ (v5 = v3) & host(v1) = v5 & % 77.66/10.91 | $i(v5)) | (host(v0) = v6 & queue(v6) = v9 & $i(v9) & $i(v6) & ~ % 77.66/10.91 | elem(v4, v9)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 77.66/10.91 | [v3: $i] : ( ~ (m_Ldr(v1) = v2) | ~ (host(v0) = v3) | ~ $i(v1) | ~ % 77.66/10.91 | $i(v0) | ? [v4: $i] : ? [v5: $i] : ((host(v1) = v5 & $i(v5) & ~ % 77.66/10.91 | leq(v3, v5)) | (queue(v3) = v4 & $i(v4) & ~ elem(v2, v4)))) & % 77.66/10.91 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) = % 77.66/10.91 | v3) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.91 | alive) | ~ setIn(v0, alive) | leq(v2, v3) | ? [v4: $i] : ? [v5: % 77.66/10.91 | $i] : ? [v6: $i] : ? [v7: $i] : (( ~ (v5 = elec_2) & % 77.66/10.91 | index(status, v3) = v5 & $i(v5)) | ( ~ (v4 = elec_2) & % 77.66/10.91 | index(status, v2) = v4 & $i(v4)) | (index(pendack, v3) = v7 & % 77.66/10.91 | index(pendack, v2) = v6 & $i(v7) & $i(v6) & ~ leq(v6, v7)))) & % 77.66/10.91 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) = % 77.66/10.91 | v3) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.91 | alive) | ~ setIn(v0, alive) | leq(v2, v3) | ? [v4: $i] : ? [v5: % 77.66/10.91 | $i] : ? [v6: $i] : (( ~ (v5 = elec_2) & index(status, v3) = v5 & % 77.66/10.91 | $i(v5)) | ( ~ (v4 = elec_2) & index(status, v2) = v4 & $i(v4)) | % 77.66/10.91 | (index(pendack, v3) = v6 & $i(v6) & leq(v6, v2)))) & ! [v0: $i] : % 77.66/10.91 | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) = v2) | ~ % 77.66/10.91 | (host(v0) = v3) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ~ % 77.66/10.91 | setIn(v0, alive) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: % 77.66/10.91 | $i] : (( ~ (v7 = norm) & index(status, v3) = v7 & $i(v7)) | ( ~ % 77.66/10.91 | (v6 = v3) & index(ldr, v3) = v6 & $i(v6)) | ( ~ (v5 = elec_2) & % 77.66/10.91 | index(status, v2) = v5 & $i(v5)) | (index(pendack, v2) = v4 & % 77.66/10.91 | $i(v4) & leq(v4, v3)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 77.66/10.91 | $i] : ! [v3: $i] : ( ~ (host(v1) = v2) | ~ (host(v0) = v3) | ~ % 77.66/10.91 | $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ~ setIn(v0, alive) | ? % 77.66/10.91 | [v4: $i] : ? [v5: $i] : ? [v6: $i] : (( ~ (v5 = v2) & index(ldr, % 77.66/10.91 | v2) = v5 & $i(v5)) | ( ~ (v4 = norm) & index(status, v2) = v4 % 77.66/10.91 | & $i(v4)) | (index(down, v3) = v6 & $i(v6) & ~ setIn(v2, v6)))) % 77.66/10.91 | & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 77.66/10.91 | (host(v1) = v2) | ~ (host(v0) = v3) | ~ $i(v1) | ~ $i(v0) | ~ % 77.66/10.91 | setIn(v1, alive) | ~ setIn(v0, alive) | ? [v4: $i] : ? [v5: $i] : % 77.66/10.91 | ? [v6: $i] : (( ~ (v5 = elec_2) & index(status, v2) = v5 & $i(v5)) % 77.66/10.91 | | (index(pendack, v2) = v6 & $i(v6) & leq(v6, v3)) | (index(down, % 77.66/10.91 | v3) = v4 & $i(v4) & ~ setIn(v2, v4)))) & ! [v0: $i] : ! % 77.66/10.91 | [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (host(v1) = v2) | ~ (host(v0) % 77.66/10.91 | = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ~ setIn(v0, % 77.66/10.91 | alive)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (m_Ack(v0, % 77.66/10.91 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ? % 77.66/10.91 | [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (( ~ (v4 = % 77.66/10.91 | elec_2) & index(status, v3) = v4 & host(v1) = v3 & $i(v4) & % 77.66/10.91 | $i(v3)) | (host(v0) = v5 & queue(v5) = v6 & $i(v6) & $i(v5) & ~ % 77.66/10.91 | elem(v2, v6)))) & ! [v0: $i] : ! [v1: $i] : ( ~ (host(v0) = % 77.66/10.91 | v1) | ~ $i(v0) | ~ setIn(v0, alive) | ? [v2: $i] : ? [v3: $i] % 77.66/10.91 | : ((v3 = v0 & index(elid, v1) = v0) | ( ~ (v2 = elec_1) & ~ (v2 = % 77.66/10.91 | elec_2) & index(status, v1) = v2 & $i(v2)))) & ! [v0: any] : % 77.66/10.91 | (v0 = all_65_8 | ~ $i(v0) | ~ leq(all_65_16, v0) | leq(all_65_11, % 77.66/10.91 | v0) | setIn(v0, all_65_4)) & ( ~ (norm = elec_1) | ( ~ (all_65_7 = % 77.66/10.91 | all_65_8) & index(ldr, all_65_11) = all_65_7 & $i(all_65_7))) & % 77.66/10.91 | ( ~ (wait = elec_1) | ( ~ (all_65_5 = all_65_8) & index(elid, % 77.66/10.91 | all_65_11) = all_65_6 & host(all_65_6) = all_65_5 & $i(all_65_5) % 77.66/10.91 | & $i(all_65_6))) % 77.66/10.91 | % 77.66/10.91 | ALPHA: (16) implies: % 77.66/10.91 | (17) ~ (all_65_1 = all_65_11) % 77.66/10.91 | (18) ~ leq(all_65_3, all_65_1) % 77.66/10.91 | (19) setIn(all_65_13, alive) % 77.66/10.91 | (20) setIn(all_65_2, alive) % 77.66/10.91 | (21) setIn(all_65_0, alive) % 77.66/10.91 | (22) $i(all_65_15) % 77.66/10.91 | (23) $i(all_65_13) % 77.66/10.91 | (24) $i(all_65_12) % 77.66/10.91 | (25) $i(all_65_11) % 77.66/10.91 | (26) $i(all_65_9) % 77.66/10.91 | (27) $i(all_65_2) % 77.66/10.91 | (28) $i(all_65_1) % 77.66/10.91 | (29) $i(all_65_0) % 77.66/10.91 | (30) queue(all_65_11) = all_65_10 % 77.66/10.91 | (31) host(all_65_13) = all_65_11 % 77.66/10.91 | (32) host(all_65_12) = all_65_8 % 77.66/10.91 | (33) host(all_65_2) = all_65_1 % 77.66/10.91 | (34) host(all_65_0) = all_65_11 % 77.66/10.91 | (35) s(zero) = all_65_16 % 77.66/10.91 | (36) s(all_65_11) = all_65_3 % 77.66/10.91 | (37) m_Down(all_65_12) = all_65_9 % 77.66/10.91 | (38) cons(all_65_9, all_65_15) = all_65_10 % 77.66/10.91 | (39) index(status, all_65_11) = elec_1 % 77.66/10.91 | (40) index(status, all_65_1) = norm % 77.66/10.91 | (41) index(down, all_65_11) = all_65_4 % 77.66/10.91 | (42) index(ldr, all_65_1) = all_65_1 % 77.66/10.91 | (43) ! [v0: any] : (v0 = all_65_8 | ~ $i(v0) | ~ leq(all_65_16, v0) | % 77.66/10.91 | leq(all_65_11, v0) | setIn(v0, all_65_4)) % 77.66/10.91 | (44) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (host(v1) = % 77.66/10.91 | v2) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.91 | alive) | ~ setIn(v0, alive)) % 77.66/10.91 | (45) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) % 77.66/10.91 | = v2) | ~ (host(v0) = v3) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.91 | alive) | ~ setIn(v0, alive) | ? [v4: $i] : ? [v5: $i] : ? [v6: % 77.66/10.91 | $i] : (( ~ (v5 = v2) & index(ldr, v2) = v5 & $i(v5)) | ( ~ (v4 = % 77.66/10.91 | norm) & index(status, v2) = v4 & $i(v4)) | (index(down, v3) = % 77.66/10.91 | v6 & $i(v6) & ~ setIn(v2, v6)))) % 77.66/10.91 | (46) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) % 77.66/10.91 | = v3) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.91 | alive) | ~ setIn(v0, alive) | leq(v2, v3) | ? [v4: $i] : ? [v5: % 77.66/10.91 | $i] : ? [v6: $i] : (( ~ (v5 = elec_2) & index(status, v3) = v5 & % 77.66/10.91 | $i(v5)) | ( ~ (v4 = elec_2) & index(status, v2) = v4 & $i(v4)) | % 77.66/10.91 | (index(pendack, v3) = v6 & $i(v6) & leq(v6, v2)))) % 77.66/10.92 | (47) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (host(v1) % 77.66/10.92 | = v3) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 77.66/10.92 | alive) | ~ setIn(v0, alive) | leq(v2, v3) | ? [v4: $i] : ? [v5: % 77.66/10.92 | $i] : ? [v6: $i] : ? [v7: $i] : (( ~ (v5 = elec_2) & % 77.66/10.92 | index(status, v3) = v5 & $i(v5)) | ( ~ (v4 = elec_2) & % 77.66/10.92 | index(status, v2) = v4 & $i(v4)) | (index(pendack, v3) = v7 & % 77.66/10.92 | index(pendack, v2) = v6 & $i(v7) & $i(v6) & ~ leq(v6, v7)))) % 77.66/10.92 | (48) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 77.66/10.92 | ! [v5: $i] : ( ~ (m_Down(v1) = v4) | ~ (host(v2) = v3) | ~ (host(v0) % 77.66/10.92 | = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v2, alive) | % 77.66/10.92 | ~ setIn(v0, alive) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 77.66/10.92 | [v9: $i] : (( ~ (v8 = v3) & index(ldr, v3) = v8 & $i(v8)) | ( ~ (v7 % 77.66/10.92 | = norm) & index(status, v3) = v7 & $i(v7)) | ( ~ (v6 = v3) & % 77.66/10.92 | host(v1) = v6 & $i(v6)) | (queue(v5) = v9 & $i(v9) & ~ elem(v4, % 77.66/10.92 | v9)))) % 77.66/10.92 | (49) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 77.66/10.92 | ! [v5: $i] : ( ~ (m_Down(v1) = v5) | ~ (host(v2) = v3) | ~ (host(v0) % 77.66/10.92 | = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v0, alive) | % 77.66/10.92 | leq(v3, v4) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] % 77.66/10.92 | : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ($i(v12) & (( ~ (v12 % 77.66/10.92 | = v7) & index(down, v3) = v6 & host(v1) = v7 & $i(v7) & % 77.66/10.92 | $i(v6) & leq(all_65_16, v12) & ~ leq(v3, v12) & ~ setIn(v12, % 77.66/10.92 | v6)) | ( ~ (v11 = norm) & index(status, v4) = v11 & $i(v11)) % 77.66/10.92 | | ( ~ (v10 = v4) & index(ldr, v4) = v10 & $i(v10)) | ( ~ (v9 = % 77.66/10.92 | elec_1) & index(status, v3) = v9 & $i(v9)) | (queue(v3) = v8 % 77.66/10.92 | & $i(v8) & ~ elem(v5, v8))))) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (12) with all_59_0, all_65_16, zero, simplifying % 77.66/10.92 | with (15), (35) gives: % 77.66/10.92 | (50) all_65_16 = all_59_0 % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (axiom_01) with all_65_2, all_65_2, all_65_1, % 77.66/10.92 | simplifying with (27), (33) gives: % 77.66/10.92 | (51) ? [v0: any] : ( ~ (v0 = all_65_1) & s(all_65_1) = v0 & $i(v0)) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (46) with all_65_2, all_65_0, all_65_1, all_65_11, % 77.66/10.92 | simplifying with (20), (21), (27), (29), (33), (34) gives: % 77.66/10.92 | (52) leq(all_65_1, all_65_11) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 77.66/10.92 | (( ~ (v1 = elec_2) & index(status, all_65_11) = v1 & $i(v1)) | ( ~ (v0 % 77.66/10.92 | = elec_2) & index(status, all_65_1) = v0 & $i(v0)) | % 77.66/10.92 | (index(pendack, all_65_11) = v2 & $i(v2) & leq(v2, all_65_1))) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (47) with all_65_0, all_65_2, all_65_11, all_65_1, % 77.66/10.92 | simplifying with (20), (21), (27), (29), (33), (34) gives: % 77.66/10.92 | (53) leq(all_65_11, all_65_1) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 77.66/10.92 | ? [v3: $i] : (( ~ (v1 = elec_2) & index(status, all_65_1) = v1 & % 77.66/10.92 | $i(v1)) | ( ~ (v0 = elec_2) & index(status, all_65_11) = v0 & % 77.66/10.92 | $i(v0)) | (index(pendack, all_65_1) = v3 & index(pendack, % 77.66/10.92 | all_65_11) = v2 & $i(v3) & $i(v2) & ~ leq(v2, v3))) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (45) with all_65_0, all_65_2, all_65_1, all_65_11, % 77.66/10.92 | simplifying with (20), (21), (27), (29), (33), (34) gives: % 77.66/10.92 | (54) ? [v0: $i] : ? [v1: any] : ? [v2: $i] : (( ~ (v1 = all_65_1) & % 77.66/10.92 | index(ldr, all_65_1) = v1 & $i(v1)) | ( ~ (v0 = norm) & % 77.66/10.92 | index(status, all_65_1) = v0 & $i(v0)) | (index(down, all_65_11) = % 77.66/10.92 | v2 & $i(v2) & ~ setIn(all_65_1, v2))) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (44) with all_65_13, all_65_0, all_65_11, % 77.66/10.92 | simplifying with (19), (21), (23), (29), (31), (34) gives: % 77.66/10.92 | (55) all_65_0 = all_65_13 % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (axiom_01) with all_65_13, all_65_0, all_65_11, % 77.66/10.92 | simplifying with (23), (29), (31), (34) gives: % 77.66/10.92 | (56) ? [v0: any] : ( ~ (v0 = all_65_11) & s(all_65_11) = v0 & $i(v0)) % 77.66/10.92 | % 77.66/10.92 | GROUND_INST: instantiating (48) with all_65_13, all_65_12, all_65_2, all_65_1, % 77.66/10.92 | all_65_9, all_65_11, simplifying with (19), (20), (23), (24), % 77.66/10.92 | (27), (31), (33), (37) gives: % 77.66/10.93 | (57) ? [v0: any] : ? [v1: $i] : ? [v2: any] : ? [v3: $i] : (( ~ (v2 = % 77.66/10.93 | all_65_1) & index(ldr, all_65_1) = v2 & $i(v2)) | ( ~ (v1 = % 77.66/10.93 | norm) & index(status, all_65_1) = v1 & $i(v1)) | ( ~ (v0 = % 77.66/10.93 | all_65_1) & host(all_65_12) = v0 & $i(v0)) | (queue(all_65_11) = % 77.66/10.93 | v3 & $i(v3) & ~ elem(all_65_9, v3))) % 77.66/10.93 | % 77.66/10.93 | GROUND_INST: instantiating (49) with all_65_13, all_65_12, all_65_2, all_65_1, % 77.66/10.93 | all_65_11, all_65_9, simplifying with (19), (23), (24), (27), % 77.66/10.93 | (31), (33), (37) gives: % 77.66/10.93 | (58) leq(all_65_1, all_65_11) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 77.66/10.93 | ? [v3: $i] : ? [v4: any] : ? [v5: $i] : ? [v6: $i] : ($i(v6) & (( ~ % 77.66/10.93 | (v6 = v1) & index(down, all_65_1) = v0 & host(all_65_12) = v1 & % 77.66/10.93 | $i(v1) & $i(v0) & leq(all_65_16, v6) & ~ leq(all_65_1, v6) & ~ % 77.66/10.93 | setIn(v6, v0)) | ( ~ (v5 = norm) & index(status, all_65_11) = v5 % 77.66/10.93 | & $i(v5)) | ( ~ (v4 = all_65_11) & index(ldr, all_65_11) = v4 & % 77.66/10.93 | $i(v4)) | ( ~ (v3 = elec_1) & index(status, all_65_1) = v3 & % 77.66/10.93 | $i(v3)) | (queue(all_65_1) = v2 & $i(v2) & ~ elem(all_65_9, % 77.66/10.93 | v2)))) % 77.66/10.93 | % 77.66/10.93 | GROUND_INST: instantiating (4) with all_65_9, all_65_12, simplifying with % 77.66/10.93 | (24), (26), (37) gives: % 77.66/10.93 | (59) pidElem(all_65_9) % 77.66/10.93 | % 77.66/10.93 | GROUND_INST: instantiating (2) with all_65_9, all_65_15, all_65_10, % 77.66/10.93 | simplifying with (22), (26), (38) gives: % 77.66/10.93 | (60) elem(all_65_9, all_65_10) % 77.66/10.93 | % 77.66/10.93 | DELTA: instantiating (51) with fresh symbol all_78_0 gives: % 77.66/10.93 | (61) ~ (all_78_0 = all_65_1) & s(all_65_1) = all_78_0 & $i(all_78_0) % 77.66/10.93 | % 77.66/10.93 | ALPHA: (61) implies: % 77.66/10.93 | (62) s(all_65_1) = all_78_0 % 77.66/10.93 | % 77.66/10.93 | DELTA: instantiating (56) with fresh symbol all_82_0 gives: % 77.66/10.93 | (63) ~ (all_82_0 = all_65_11) & s(all_65_11) = all_82_0 & $i(all_82_0) % 77.66/10.93 | % 77.66/10.93 | ALPHA: (63) implies: % 77.66/10.93 | (64) $i(all_82_0) % 77.66/10.93 | (65) s(all_65_11) = all_82_0 % 77.66/10.93 | % 77.66/10.93 | DELTA: instantiating (54) with fresh symbols all_94_0, all_94_1, all_94_2 % 77.66/10.93 | gives: % 77.66/10.93 | (66) ( ~ (all_94_1 = all_65_1) & index(ldr, all_65_1) = all_94_1 & % 77.66/10.93 | $i(all_94_1)) | ( ~ (all_94_2 = norm) & index(status, all_65_1) = % 77.66/10.93 | all_94_2 & $i(all_94_2)) | (index(down, all_65_11) = all_94_0 & % 77.66/10.93 | $i(all_94_0) & ~ setIn(all_65_1, all_94_0)) % 77.66/10.93 | % 77.66/10.93 | DELTA: instantiating (57) with fresh symbols all_103_0, all_103_1, all_103_2, % 77.66/10.93 | all_103_3 gives: % 77.66/10.93 | (67) ( ~ (all_103_1 = all_65_1) & index(ldr, all_65_1) = all_103_1 & % 77.66/10.93 | $i(all_103_1)) | ( ~ (all_103_2 = norm) & index(status, all_65_1) = % 77.66/10.93 | all_103_2 & $i(all_103_2)) | ( ~ (all_103_3 = all_65_1) & % 77.66/10.93 | host(all_65_12) = all_103_3 & $i(all_103_3)) | (queue(all_65_11) = % 77.66/10.93 | all_103_0 & $i(all_103_0) & ~ elem(all_65_9, all_103_0)) % 77.66/10.93 | % 77.66/10.93 | BETA: splitting (67) gives: % 77.66/10.93 | % 77.66/10.93 | Case 1: % 77.66/10.93 | | % 77.66/10.93 | | (68) ( ~ (all_103_1 = all_65_1) & index(ldr, all_65_1) = all_103_1 & % 77.66/10.93 | | $i(all_103_1)) | ( ~ (all_103_2 = norm) & index(status, all_65_1) % 77.66/10.93 | | = all_103_2 & $i(all_103_2)) % 77.66/10.93 | | % 77.66/10.93 | | BETA: splitting (68) gives: % 77.66/10.93 | | % 77.66/10.93 | | Case 1: % 77.66/10.93 | | | % 77.66/10.93 | | | (69) ~ (all_103_1 = all_65_1) & index(ldr, all_65_1) = all_103_1 & % 77.66/10.93 | | | $i(all_103_1) % 77.66/10.93 | | | % 77.66/10.93 | | | ALPHA: (69) implies: % 77.66/10.93 | | | (70) ~ (all_103_1 = all_65_1) % 77.66/10.93 | | | (71) index(ldr, all_65_1) = all_103_1 % 77.66/10.93 | | | % 77.66/10.93 | | | GROUND_INST: instantiating (13) with all_65_1, all_103_1, all_65_1, ldr, % 77.66/10.93 | | | simplifying with (42), (71) gives: % 77.66/10.93 | | | (72) all_103_1 = all_65_1 % 77.66/10.93 | | | % 77.66/10.93 | | | REDUCE: (70), (72) imply: % 77.66/10.93 | | | (73) $false % 77.66/10.93 | | | % 77.66/10.93 | | | CLOSE: (73) is inconsistent. % 77.66/10.93 | | | % 77.66/10.93 | | Case 2: % 77.66/10.93 | | | % 77.66/10.93 | | | (74) ~ (all_103_2 = norm) & index(status, all_65_1) = all_103_2 & % 77.66/10.93 | | | $i(all_103_2) % 77.66/10.93 | | | % 77.66/10.93 | | | ALPHA: (74) implies: % 77.66/10.93 | | | (75) ~ (all_103_2 = norm) % 77.66/10.93 | | | (76) index(status, all_65_1) = all_103_2 % 77.66/10.93 | | | % 77.66/10.93 | | | GROUND_INST: instantiating (13) with norm, all_103_2, all_65_1, status, % 77.66/10.93 | | | simplifying with (40), (76) gives: % 77.66/10.93 | | | (77) all_103_2 = norm % 77.66/10.93 | | | % 77.66/10.93 | | | REDUCE: (75), (77) imply: % 77.66/10.93 | | | (78) $false % 77.66/10.93 | | | % 77.66/10.93 | | | CLOSE: (78) is inconsistent. % 77.66/10.93 | | | % 77.66/10.93 | | End of split % 77.66/10.93 | | % 77.66/10.93 | Case 2: % 77.66/10.93 | | % 77.66/10.93 | | (79) ( ~ (all_103_3 = all_65_1) & host(all_65_12) = all_103_3 & % 77.66/10.93 | | $i(all_103_3)) | (queue(all_65_11) = all_103_0 & $i(all_103_0) & % 77.66/10.93 | | ~ elem(all_65_9, all_103_0)) % 77.66/10.93 | | % 77.66/10.93 | | BETA: splitting (79) gives: % 77.66/10.93 | | % 77.66/10.93 | | Case 1: % 77.66/10.93 | | | % 77.66/10.93 | | | (80) ~ (all_103_3 = all_65_1) & host(all_65_12) = all_103_3 & % 77.66/10.93 | | | $i(all_103_3) % 77.66/10.93 | | | % 77.66/10.93 | | | ALPHA: (80) implies: % 77.66/10.93 | | | (81) host(all_65_12) = all_103_3 % 77.66/10.93 | | | % 77.66/10.93 | | | BETA: splitting (66) gives: % 77.66/10.93 | | | % 77.66/10.93 | | | Case 1: % 77.66/10.93 | | | | % 77.66/10.93 | | | | (82) ~ (all_94_1 = all_65_1) & index(ldr, all_65_1) = all_94_1 & % 77.66/10.93 | | | | $i(all_94_1) % 77.66/10.93 | | | | % 77.66/10.93 | | | | ALPHA: (82) implies: % 77.66/10.93 | | | | (83) ~ (all_94_1 = all_65_1) % 77.66/10.93 | | | | (84) index(ldr, all_65_1) = all_94_1 % 77.66/10.93 | | | | % 77.66/10.93 | | | | GROUND_INST: instantiating (13) with all_65_1, all_94_1, all_65_1, ldr, % 77.66/10.93 | | | | simplifying with (42), (84) gives: % 77.66/10.93 | | | | (85) all_94_1 = all_65_1 % 77.66/10.93 | | | | % 77.66/10.93 | | | | REDUCE: (83), (85) imply: % 77.66/10.93 | | | | (86) $false % 77.66/10.93 | | | | % 77.66/10.93 | | | | CLOSE: (86) is inconsistent. % 77.66/10.93 | | | | % 77.66/10.93 | | | Case 2: % 77.66/10.93 | | | | % 77.66/10.93 | | | | (87) ( ~ (all_94_2 = norm) & index(status, all_65_1) = all_94_2 & % 77.66/10.93 | | | | $i(all_94_2)) | (index(down, all_65_11) = all_94_0 & % 77.66/10.93 | | | | $i(all_94_0) & ~ setIn(all_65_1, all_94_0)) % 77.66/10.93 | | | | % 77.66/10.93 | | | | BETA: splitting (87) gives: % 77.66/10.93 | | | | % 77.66/10.93 | | | | Case 1: % 77.66/10.93 | | | | | % 77.66/10.94 | | | | | (88) ~ (all_94_2 = norm) & index(status, all_65_1) = all_94_2 & % 77.66/10.94 | | | | | $i(all_94_2) % 77.66/10.94 | | | | | % 77.66/10.94 | | | | | ALPHA: (88) implies: % 77.66/10.94 | | | | | (89) ~ (all_94_2 = norm) % 78.08/10.94 | | | | | (90) index(status, all_65_1) = all_94_2 % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | GROUND_INST: instantiating (13) with norm, all_94_2, all_65_1, status, % 78.08/10.94 | | | | | simplifying with (40), (90) gives: % 78.08/10.94 | | | | | (91) all_94_2 = norm % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | REDUCE: (89), (91) imply: % 78.08/10.94 | | | | | (92) $false % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | CLOSE: (92) is inconsistent. % 78.08/10.94 | | | | | % 78.08/10.94 | | | | Case 2: % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | (93) index(down, all_65_11) = all_94_0 & $i(all_94_0) & ~ % 78.08/10.94 | | | | | setIn(all_65_1, all_94_0) % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | ALPHA: (93) implies: % 78.08/10.94 | | | | | (94) index(down, all_65_11) = all_94_0 % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | GROUND_INST: instantiating (11) with all_65_8, all_103_3, all_65_12, % 78.08/10.94 | | | | | simplifying with (32), (81) gives: % 78.08/10.94 | | | | | (95) all_103_3 = all_65_8 % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | GROUND_INST: instantiating (12) with all_65_3, all_82_0, all_65_11, % 78.08/10.94 | | | | | simplifying with (36), (65) gives: % 78.08/10.94 | | | | | (96) all_82_0 = all_65_3 % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | GROUND_INST: instantiating (13) with all_65_4, all_94_0, all_65_11, % 78.08/10.94 | | | | | down, simplifying with (41), (94) gives: % 78.08/10.94 | | | | | (97) all_94_0 = all_65_4 % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | REDUCE: (64), (96) imply: % 78.08/10.94 | | | | | (98) $i(all_65_3) % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | GROUND_INST: instantiating (3) with all_65_9, simplifying with (26), % 78.08/10.94 | | | | | (59) gives: % 78.08/10.94 | | | | | (99) ? [v0: $i] : ? [v1: int] : ? [v2: int] : ($i(v0) & ((v2 = % 78.08/10.94 | | | | | all_65_9 & m_Down(v0) = all_65_9) | (v1 = all_65_9 & % 78.08/10.94 | | | | | m_Halt(v0) = all_65_9))) % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | DELTA: instantiating (99) with fresh symbols all_141_0, all_141_1, % 78.08/10.94 | | | | | all_141_2 gives: % 78.08/10.94 | | | | | (100) $i(all_141_2) & ((all_141_0 = all_65_9 & m_Down(all_141_2) = % 78.08/10.94 | | | | | all_65_9) | (all_141_1 = all_65_9 & m_Halt(all_141_2) = % 78.08/10.94 | | | | | all_65_9)) % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | ALPHA: (100) implies: % 78.08/10.94 | | | | | (101) $i(all_141_2) % 78.08/10.94 | | | | | (102) (all_141_0 = all_65_9 & m_Down(all_141_2) = all_65_9) | % 78.08/10.94 | | | | | (all_141_1 = all_65_9 & m_Halt(all_141_2) = all_65_9) % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | BETA: splitting (53) gives: % 78.08/10.94 | | | | | % 78.08/10.94 | | | | | Case 1: % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | (103) leq(all_65_11, all_65_1) % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | BETA: splitting (52) gives: % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | Case 1: % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | (104) leq(all_65_1, all_65_11) % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | GROUND_INST: instantiating (5) with all_65_11, all_65_1, % 78.08/10.94 | | | | | | | simplifying with (25), (28), (103), (104) gives: % 78.08/10.94 | | | | | | | (105) all_65_1 = all_65_11 % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | REDUCE: (17), (105) imply: % 78.08/10.94 | | | | | | | (106) $false % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | CLOSE: (106) is inconsistent. % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | Case 2: % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | (107) ~ leq(all_65_1, all_65_11) % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | BETA: splitting (58) gives: % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | Case 1: % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | (108) leq(all_65_1, all_65_11) % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | PRED_UNIFY: (107), (108) imply: % 78.08/10.94 | | | | | | | | (109) $false % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | CLOSE: (109) is inconsistent. % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | Case 2: % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | GROUND_INST: instantiating (6) with all_65_11, all_65_1, % 78.08/10.94 | | | | | | | | all_65_3, all_78_0, simplifying with (25), (28), % 78.08/10.94 | | | | | | | | (36), (62), (103) gives: % 78.08/10.94 | | | | | | | | (110) leq(all_65_3, all_78_0) % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | GROUND_INST: instantiating (8) with all_65_3, all_65_1, % 78.08/10.94 | | | | | | | | all_78_0, simplifying with (18), (28), (62), (98), % 78.08/10.94 | | | | | | | | (110) gives: % 78.08/10.94 | | | | | | | | (111) all_78_0 = all_65_3 % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | REDUCE: (62), (111) imply: % 78.08/10.94 | | | | | | | | (112) s(all_65_1) = all_65_3 % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | REDUCE: (110), (111) imply: % 78.08/10.94 | | | | | | | | (113) leq(all_65_3, all_65_3) % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | GROUND_INST: instantiating (7) with all_65_1, all_65_11, % 78.08/10.94 | | | | | | | | all_65_3, all_65_3, simplifying with (25), (28), % 78.08/10.94 | | | | | | | | (36), (107), (112), (113) gives: % 78.08/10.94 | | | | | | | | (114) $false % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | | CLOSE: (114) is inconsistent. % 78.08/10.94 | | | | | | | | % 78.08/10.94 | | | | | | | End of split % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | End of split % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | Case 2: % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | (115) ~ leq(all_65_11, all_65_1) % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | BETA: splitting (102) gives: % 78.08/10.94 | | | | | | % 78.08/10.94 | | | | | | Case 1: % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | (116) all_141_0 = all_65_9 & m_Down(all_141_2) = all_65_9 % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | ALPHA: (116) implies: % 78.08/10.94 | | | | | | | (117) m_Down(all_141_2) = all_65_9 % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | GROUND_INST: instantiating (48) with all_65_13, all_141_2, % 78.08/10.94 | | | | | | | all_65_2, all_65_1, all_65_9, all_65_11, simplifying % 78.08/10.94 | | | | | | | with (19), (20), (23), (27), (31), (33), (101), (117) % 78.08/10.94 | | | | | | | gives: % 78.08/10.94 | | | | | | | (118) ? [v0: any] : ? [v1: $i] : ? [v2: any] : ? [v3: $i] : % 78.08/10.94 | | | | | | | (( ~ (v2 = all_65_1) & index(ldr, all_65_1) = v2 & % 78.08/10.94 | | | | | | | $i(v2)) | ( ~ (v1 = norm) & index(status, all_65_1) = % 78.08/10.94 | | | | | | | v1 & $i(v1)) | ( ~ (v0 = all_65_1) & host(all_141_2) % 78.08/10.94 | | | | | | | = v0 & $i(v0)) | (queue(all_65_11) = v3 & $i(v3) & ~ % 78.08/10.94 | | | | | | | elem(all_65_9, v3))) % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | GROUND_INST: instantiating (49) with all_65_2, all_141_2, % 78.08/10.94 | | | | | | | all_65_13, all_65_11, all_65_1, all_65_9, simplifying % 78.08/10.94 | | | | | | | with (20), (23), (27), (31), (33), (101), (115), % 78.08/10.94 | | | | | | | (117) gives: % 78.08/10.94 | | | | | | | (119) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 78.08/10.94 | | | | | | | ? [v4: any] : ? [v5: $i] : ? [v6: $i] : ($i(v6) & (( ~ % 78.08/10.94 | | | | | | | (v6 = v1) & index(down, all_65_11) = v0 & % 78.08/10.94 | | | | | | | host(all_141_2) = v1 & $i(v1) & $i(v0) & % 78.08/10.94 | | | | | | | leq(all_65_16, v6) & ~ leq(all_65_11, v6) & ~ % 78.08/10.94 | | | | | | | setIn(v6, v0)) | ( ~ (v5 = norm) & index(status, % 78.08/10.94 | | | | | | | all_65_1) = v5 & $i(v5)) | ( ~ (v4 = all_65_1) & % 78.08/10.94 | | | | | | | index(ldr, all_65_1) = v4 & $i(v4)) | ( ~ (v3 = % 78.08/10.94 | | | | | | | elec_1) & index(status, all_65_11) = v3 & $i(v3)) % 78.08/10.94 | | | | | | | | (queue(all_65_11) = v2 & $i(v2) & ~ elem(all_65_9, % 78.08/10.94 | | | | | | | v2)))) % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | GROUND_INST: instantiating (axiom_30) with all_65_12, all_141_2, % 78.08/10.94 | | | | | | | all_65_9, simplifying with (24), (37), (101), (117) % 78.08/10.94 | | | | | | | gives: % 78.08/10.94 | | | | | | | (120) all_141_2 = all_65_12 % 78.08/10.94 | | | | | | | % 78.08/10.94 | | | | | | | DELTA: instantiating (118) with fresh symbols all_558_0, % 78.08/10.94 | | | | | | | all_558_1, all_558_2, all_558_3 gives: % 78.08/10.95 | | | | | | | (121) ( ~ (all_558_1 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.95 | | | | | | | all_558_1 & $i(all_558_1)) | ( ~ (all_558_2 = norm) & % 78.08/10.95 | | | | | | | index(status, all_65_1) = all_558_2 & $i(all_558_2)) | % 78.08/10.95 | | | | | | | ( ~ (all_558_3 = all_65_1) & host(all_141_2) = all_558_3 % 78.08/10.95 | | | | | | | & $i(all_558_3)) | (queue(all_65_11) = all_558_0 & % 78.08/10.95 | | | | | | | $i(all_558_0) & ~ elem(all_65_9, all_558_0)) % 78.08/10.95 | | | | | | | % 78.08/10.95 | | | | | | | DELTA: instantiating (119) with fresh symbols all_570_0, % 78.08/10.95 | | | | | | | all_570_1, all_570_2, all_570_3, all_570_4, all_570_5, % 78.08/10.95 | | | | | | | all_570_6 gives: % 78.08/10.95 | | | | | | | (122) $i(all_570_0) & (( ~ (all_570_0 = all_570_5) & % 78.08/10.95 | | | | | | | index(down, all_65_11) = all_570_6 & host(all_141_2) % 78.08/10.95 | | | | | | | = all_570_5 & $i(all_570_5) & $i(all_570_6) & % 78.08/10.95 | | | | | | | leq(all_65_16, all_570_0) & ~ leq(all_65_11, % 78.08/10.95 | | | | | | | all_570_0) & ~ setIn(all_570_0, all_570_6)) | ( ~ % 78.08/10.95 | | | | | | | (all_570_1 = norm) & index(status, all_65_1) = % 78.08/10.95 | | | | | | | all_570_1 & $i(all_570_1)) | ( ~ (all_570_2 = % 78.08/10.95 | | | | | | | all_65_1) & index(ldr, all_65_1) = all_570_2 & % 78.08/10.95 | | | | | | | $i(all_570_2)) | ( ~ (all_570_3 = elec_1) & % 78.08/10.95 | | | | | | | index(status, all_65_11) = all_570_3 & $i(all_570_3)) % 78.08/10.95 | | | | | | | | (queue(all_65_11) = all_570_4 & $i(all_570_4) & ~ % 78.08/10.95 | | | | | | | elem(all_65_9, all_570_4))) % 78.08/10.95 | | | | | | | % 78.08/10.95 | | | | | | | ALPHA: (122) implies: % 78.08/10.95 | | | | | | | (123) $i(all_570_0) % 78.08/10.95 | | | | | | | (124) ( ~ (all_570_0 = all_570_5) & index(down, all_65_11) = % 78.08/10.95 | | | | | | | all_570_6 & host(all_141_2) = all_570_5 & $i(all_570_5) % 78.08/10.95 | | | | | | | & $i(all_570_6) & leq(all_65_16, all_570_0) & ~ % 78.08/10.95 | | | | | | | leq(all_65_11, all_570_0) & ~ setIn(all_570_0, % 78.08/10.95 | | | | | | | all_570_6)) | ( ~ (all_570_1 = norm) & index(status, % 78.08/10.95 | | | | | | | all_65_1) = all_570_1 & $i(all_570_1)) | ( ~ % 78.08/10.95 | | | | | | | (all_570_2 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.95 | | | | | | | all_570_2 & $i(all_570_2)) | ( ~ (all_570_3 = elec_1) & % 78.08/10.95 | | | | | | | index(status, all_65_11) = all_570_3 & $i(all_570_3)) | % 78.08/10.95 | | | | | | | (queue(all_65_11) = all_570_4 & $i(all_570_4) & ~ % 78.08/10.95 | | | | | | | elem(all_65_9, all_570_4)) % 78.08/10.95 | | | | | | | % 78.08/10.95 | | | | | | | BETA: splitting (121) gives: % 78.08/10.95 | | | | | | | % 78.08/10.95 | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | (125) ( ~ (all_558_1 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.95 | | | | | | | | all_558_1 & $i(all_558_1)) | ( ~ (all_558_2 = norm) & % 78.08/10.95 | | | | | | | | index(status, all_65_1) = all_558_2 & $i(all_558_2)) % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | BETA: splitting (125) gives: % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | (126) ~ (all_558_1 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.95 | | | | | | | | | all_558_1 & $i(all_558_1) % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | ALPHA: (126) implies: % 78.08/10.95 | | | | | | | | | (127) ~ (all_558_1 = all_65_1) % 78.08/10.95 | | | | | | | | | (128) index(ldr, all_65_1) = all_558_1 % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | GROUND_INST: instantiating (13) with all_65_1, all_558_1, % 78.08/10.95 | | | | | | | | | all_65_1, ldr, simplifying with (42), (128) gives: % 78.08/10.95 | | | | | | | | | (129) all_558_1 = all_65_1 % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | REDUCE: (127), (129) imply: % 78.08/10.95 | | | | | | | | | (130) $false % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | CLOSE: (130) is inconsistent. % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | Case 2: % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | (131) ~ (all_558_2 = norm) & index(status, all_65_1) = % 78.08/10.95 | | | | | | | | | all_558_2 & $i(all_558_2) % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | ALPHA: (131) implies: % 78.08/10.95 | | | | | | | | | (132) ~ (all_558_2 = norm) % 78.08/10.95 | | | | | | | | | (133) index(status, all_65_1) = all_558_2 % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | GROUND_INST: instantiating (13) with norm, all_558_2, all_65_1, % 78.08/10.95 | | | | | | | | | status, simplifying with (40), (133) gives: % 78.08/10.95 | | | | | | | | | (134) all_558_2 = norm % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | REDUCE: (132), (134) imply: % 78.08/10.95 | | | | | | | | | (135) $false % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | CLOSE: (135) is inconsistent. % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | End of split % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | Case 2: % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | (136) ( ~ (all_558_3 = all_65_1) & host(all_141_2) = % 78.08/10.95 | | | | | | | | all_558_3 & $i(all_558_3)) | (queue(all_65_11) = % 78.08/10.95 | | | | | | | | all_558_0 & $i(all_558_0) & ~ elem(all_65_9, % 78.08/10.95 | | | | | | | | all_558_0)) % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | BETA: splitting (136) gives: % 78.08/10.95 | | | | | | | | % 78.08/10.95 | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | (137) ~ (all_558_3 = all_65_1) & host(all_141_2) = % 78.08/10.95 | | | | | | | | | all_558_3 & $i(all_558_3) % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | ALPHA: (137) implies: % 78.08/10.95 | | | | | | | | | (138) host(all_141_2) = all_558_3 % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | REDUCE: (120), (138) imply: % 78.08/10.95 | | | | | | | | | (139) host(all_65_12) = all_558_3 % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | BETA: splitting (124) gives: % 78.08/10.95 | | | | | | | | | % 78.08/10.95 | | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | (140) ( ~ (all_570_0 = all_570_5) & index(down, % 78.08/10.95 | | | | | | | | | | all_65_11) = all_570_6 & host(all_141_2) = % 78.08/10.95 | | | | | | | | | | all_570_5 & $i(all_570_5) & $i(all_570_6) & % 78.08/10.95 | | | | | | | | | | leq(all_65_16, all_570_0) & ~ leq(all_65_11, % 78.08/10.95 | | | | | | | | | | all_570_0) & ~ setIn(all_570_0, all_570_6)) | % 78.08/10.95 | | | | | | | | | | ( ~ (all_570_1 = norm) & index(status, all_65_1) = % 78.08/10.95 | | | | | | | | | | all_570_1 & $i(all_570_1)) % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | BETA: splitting (140) gives: % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | (141) ~ (all_570_0 = all_570_5) & index(down, % 78.08/10.95 | | | | | | | | | | | all_65_11) = all_570_6 & host(all_141_2) = % 78.08/10.95 | | | | | | | | | | | all_570_5 & $i(all_570_5) & $i(all_570_6) & % 78.08/10.95 | | | | | | | | | | | leq(all_65_16, all_570_0) & ~ leq(all_65_11, % 78.08/10.95 | | | | | | | | | | | all_570_0) & ~ setIn(all_570_0, all_570_6) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | ALPHA: (141) implies: % 78.08/10.95 | | | | | | | | | | | (142) ~ (all_570_0 = all_570_5) % 78.08/10.95 | | | | | | | | | | | (143) ~ setIn(all_570_0, all_570_6) % 78.08/10.95 | | | | | | | | | | | (144) ~ leq(all_65_11, all_570_0) % 78.08/10.95 | | | | | | | | | | | (145) leq(all_65_16, all_570_0) % 78.08/10.95 | | | | | | | | | | | (146) host(all_141_2) = all_570_5 % 78.08/10.95 | | | | | | | | | | | (147) index(down, all_65_11) = all_570_6 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | REDUCE: (120), (146) imply: % 78.08/10.95 | | | | | | | | | | | (148) host(all_65_12) = all_570_5 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | REDUCE: (50), (145) imply: % 78.08/10.95 | | | | | | | | | | | (149) leq(all_59_0, all_570_0) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | GROUND_INST: instantiating (11) with all_65_8, all_570_5, % 78.08/10.95 | | | | | | | | | | | all_65_12, simplifying with (32), (148) gives: % 78.08/10.95 | | | | | | | | | | | (150) all_570_5 = all_65_8 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | GROUND_INST: instantiating (11) with all_558_3, all_570_5, % 78.08/10.95 | | | | | | | | | | | all_65_12, simplifying with (139), (148) gives: % 78.08/10.95 | | | | | | | | | | | (151) all_570_5 = all_558_3 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_65_4, all_570_6, % 78.08/10.95 | | | | | | | | | | | all_65_11, down, simplifying with (41), (147) % 78.08/10.95 | | | | | | | | | | | gives: % 78.08/10.95 | | | | | | | | | | | (152) all_570_6 = all_65_4 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | COMBINE_EQS: (150), (151) imply: % 78.08/10.95 | | | | | | | | | | | (153) all_558_3 = all_65_8 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | REDUCE: (142), (150) imply: % 78.08/10.95 | | | | | | | | | | | (154) ~ (all_570_0 = all_65_8) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | REDUCE: (143), (152) imply: % 78.08/10.95 | | | | | | | | | | | (155) ~ setIn(all_570_0, all_65_4) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | GROUND_INST: instantiating (43) with all_570_0, simplifying % 78.08/10.95 | | | | | | | | | | | with (123), (144), (155) gives: % 78.08/10.95 | | | | | | | | | | | (156) all_570_0 = all_65_8 | ~ leq(all_65_16, % 78.08/10.95 | | | | | | | | | | | all_570_0) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | BETA: splitting (156) gives: % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | (157) ~ leq(all_65_16, all_570_0) % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | REDUCE: (50), (157) imply: % 78.08/10.95 | | | | | | | | | | | | (158) ~ leq(all_59_0, all_570_0) % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | PRED_UNIFY: (149), (158) imply: % 78.08/10.95 | | | | | | | | | | | | (159) $false % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | CLOSE: (159) is inconsistent. % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | Case 2: % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | (160) all_570_0 = all_65_8 % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | REDUCE: (154), (160) imply: % 78.08/10.95 | | | | | | | | | | | | (161) $false % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | | CLOSE: (161) is inconsistent. % 78.08/10.95 | | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | End of split % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | Case 2: % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | (162) ~ (all_570_1 = norm) & index(status, all_65_1) = % 78.08/10.95 | | | | | | | | | | | all_570_1 & $i(all_570_1) % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | ALPHA: (162) implies: % 78.08/10.95 | | | | | | | | | | | (163) ~ (all_570_1 = norm) % 78.08/10.95 | | | | | | | | | | | (164) index(status, all_65_1) = all_570_1 % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | GROUND_INST: instantiating (13) with norm, all_570_1, all_65_1, % 78.08/10.95 | | | | | | | | | | | status, simplifying with (40), (164) gives: % 78.08/10.95 | | | | | | | | | | | (165) all_570_1 = norm % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | REDUCE: (163), (165) imply: % 78.08/10.95 | | | | | | | | | | | (166) $false % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | | CLOSE: (166) is inconsistent. % 78.08/10.95 | | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | End of split % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | Case 2: % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | (167) ( ~ (all_570_2 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.95 | | | | | | | | | | all_570_2 & $i(all_570_2)) | ( ~ (all_570_3 = % 78.08/10.95 | | | | | | | | | | elec_1) & index(status, all_65_11) = all_570_3 % 78.08/10.95 | | | | | | | | | | & $i(all_570_3)) | (queue(all_65_11) = all_570_4 % 78.08/10.95 | | | | | | | | | | & $i(all_570_4) & ~ elem(all_65_9, all_570_4)) % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | BETA: splitting (167) gives: % 78.08/10.95 | | | | | | | | | | % 78.08/10.95 | | | | | | | | | | Case 1: % 78.08/10.95 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | (168) ~ (all_570_2 = all_65_1) & index(ldr, all_65_1) = % 78.08/10.96 | | | | | | | | | | | all_570_2 & $i(all_570_2) % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | ALPHA: (168) implies: % 78.08/10.96 | | | | | | | | | | | (169) ~ (all_570_2 = all_65_1) % 78.08/10.96 | | | | | | | | | | | (170) index(ldr, all_65_1) = all_570_2 % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | GROUND_INST: instantiating (13) with all_65_1, all_570_2, % 78.08/10.96 | | | | | | | | | | | all_65_1, ldr, simplifying with (42), (170) gives: % 78.08/10.96 | | | | | | | | | | | (171) all_570_2 = all_65_1 % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | REDUCE: (169), (171) imply: % 78.08/10.96 | | | | | | | | | | | (172) $false % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | CLOSE: (172) is inconsistent. % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | Case 2: % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | (173) ( ~ (all_570_3 = elec_1) & index(status, % 78.08/10.96 | | | | | | | | | | | all_65_11) = all_570_3 & $i(all_570_3)) | % 78.08/10.96 | | | | | | | | | | | (queue(all_65_11) = all_570_4 & $i(all_570_4) & ~ % 78.08/10.96 | | | | | | | | | | | elem(all_65_9, all_570_4)) % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | BETA: splitting (173) gives: % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | Case 1: % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | (174) ~ (all_570_3 = elec_1) & index(status, all_65_11) % 78.08/10.96 | | | | | | | | | | | | = all_570_3 & $i(all_570_3) % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | ALPHA: (174) implies: % 78.08/10.96 | | | | | | | | | | | | (175) ~ (all_570_3 = elec_1) % 78.08/10.96 | | | | | | | | | | | | (176) index(status, all_65_11) = all_570_3 % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | GROUND_INST: instantiating (13) with elec_1, all_570_3, % 78.08/10.96 | | | | | | | | | | | | all_65_11, status, simplifying with (39), (176) % 78.08/10.96 | | | | | | | | | | | | gives: % 78.08/10.96 | | | | | | | | | | | | (177) all_570_3 = elec_1 % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | REDUCE: (175), (177) imply: % 78.08/10.96 | | | | | | | | | | | | (178) $false % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | CLOSE: (178) is inconsistent. % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | Case 2: % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | (179) queue(all_65_11) = all_570_4 & $i(all_570_4) & ~ % 78.08/10.96 | | | | | | | | | | | | elem(all_65_9, all_570_4) % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | ALPHA: (179) implies: % 78.08/10.96 | | | | | | | | | | | | (180) ~ elem(all_65_9, all_570_4) % 78.08/10.96 | | | | | | | | | | | | (181) queue(all_65_11) = all_570_4 % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_65_10, all_570_4, % 78.08/10.96 | | | | | | | | | | | | all_65_11, simplifying with (30), (181) gives: % 78.08/10.96 | | | | | | | | | | | | (182) all_570_4 = all_65_10 % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | REDUCE: (180), (182) imply: % 78.08/10.96 | | | | | | | | | | | | (183) ~ elem(all_65_9, all_65_10) % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | PRED_UNIFY: (60), (183) imply: % 78.08/10.96 | | | | | | | | | | | | (184) $false % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | | CLOSE: (184) is inconsistent. % 78.08/10.96 | | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | | End of split % 78.08/10.96 | | | | | | | | | | | % 78.08/10.96 | | | | | | | | | | End of split % 78.08/10.96 | | | | | | | | | | % 78.08/10.96 | | | | | | | | | End of split % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | Case 2: % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | (185) queue(all_65_11) = all_558_0 & $i(all_558_0) & ~ % 78.08/10.96 | | | | | | | | | elem(all_65_9, all_558_0) % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | ALPHA: (185) implies: % 78.08/10.96 | | | | | | | | | (186) ~ elem(all_65_9, all_558_0) % 78.08/10.96 | | | | | | | | | (187) queue(all_65_11) = all_558_0 % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | GROUND_INST: instantiating (10) with all_65_10, all_558_0, % 78.08/10.96 | | | | | | | | | all_65_11, simplifying with (30), (187) gives: % 78.08/10.96 | | | | | | | | | (188) all_558_0 = all_65_10 % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | REDUCE: (186), (188) imply: % 78.08/10.96 | | | | | | | | | (189) ~ elem(all_65_9, all_65_10) % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | PRED_UNIFY: (60), (189) imply: % 78.08/10.96 | | | | | | | | | (190) $false % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | | CLOSE: (190) is inconsistent. % 78.08/10.96 | | | | | | | | | % 78.08/10.96 | | | | | | | | End of split % 78.08/10.96 | | | | | | | | % 78.08/10.96 | | | | | | | End of split % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | Case 2: % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | | (191) all_141_1 = all_65_9 & m_Halt(all_141_2) = all_65_9 % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | | ALPHA: (191) implies: % 78.08/10.96 | | | | | | | (192) m_Halt(all_141_2) = all_65_9 % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | | GROUND_INST: instantiating (axiom_17) with all_65_12, all_141_2, % 78.08/10.96 | | | | | | | all_65_9, simplifying with (24), (37), (101), (192) % 78.08/10.96 | | | | | | | gives: % 78.08/10.96 | | | | | | | (193) $false % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | | CLOSE: (193) is inconsistent. % 78.08/10.96 | | | | | | | % 78.08/10.96 | | | | | | End of split % 78.08/10.96 | | | | | | % 78.08/10.96 | | | | | End of split % 78.08/10.96 | | | | | % 78.08/10.96 | | | | End of split % 78.08/10.96 | | | | % 78.08/10.96 | | | End of split % 78.08/10.96 | | | % 78.08/10.96 | | Case 2: % 78.08/10.96 | | | % 78.08/10.96 | | | (194) queue(all_65_11) = all_103_0 & $i(all_103_0) & ~ elem(all_65_9, % 78.08/10.96 | | | all_103_0) % 78.08/10.96 | | | % 78.08/10.96 | | | ALPHA: (194) implies: % 78.08/10.96 | | | (195) ~ elem(all_65_9, all_103_0) % 78.08/10.96 | | | (196) queue(all_65_11) = all_103_0 % 78.08/10.96 | | | % 78.08/10.96 | | | GROUND_INST: instantiating (10) with all_65_10, all_103_0, all_65_11, % 78.08/10.96 | | | simplifying with (30), (196) gives: % 78.08/10.96 | | | (197) all_103_0 = all_65_10 % 78.08/10.96 | | | % 78.08/10.96 | | | REDUCE: (195), (197) imply: % 78.08/10.96 | | | (198) ~ elem(all_65_9, all_65_10) % 78.08/10.96 | | | % 78.08/10.96 | | | PRED_UNIFY: (60), (198) imply: % 78.08/10.96 | | | (199) $false % 78.08/10.96 | | | % 78.08/10.96 | | | CLOSE: (199) is inconsistent. % 78.08/10.96 | | | % 78.08/10.96 | | End of split % 78.08/10.96 | | % 78.08/10.96 | End of split % 78.08/10.96 | % 78.08/10.96 End of proof % 78.08/10.96 % SZS output end Proof for theBenchmark % 78.08/10.96 % 78.08/10.96 10325ms %------------------------------------------------------------------------------