%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV465+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 : n003.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:36 EDT 2023 % Result : Theorem 69.68s 9.67s % Output : Proof 70.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWV465+1 : TPTP v8.1.2. Released v4.0.0. % 0.04/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n003.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 10:50:25 EDT 2023 % 0.19/0.33 % CPUTime : % 0.19/0.53 ________ _____ % 0.19/0.53 ___ __ \_________(_)________________________________ % 0.19/0.53 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.53 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.53 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.53 % 0.19/0.53 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.53 (2023-06-19) % 0.19/0.53 % 0.19/0.53 (c) Philipp Rümmer, 2009-2023 % 0.19/0.53 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.53 Amanda Stjerna. % 0.19/0.53 Free software under BSD-3-Clause. % 0.19/0.53 % 0.19/0.53 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.53 % 0.19/0.53 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.54 Running up to 7 provers in parallel. % 0.19/0.55 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.55 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.55 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.55 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.55 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.55 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.55 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.77/1.17 Prover 1: Preprocessing ... % 3.77/1.17 Prover 4: Preprocessing ... % 4.16/1.21 Prover 0: Preprocessing ... % 4.16/1.21 Prover 2: Preprocessing ... % 4.16/1.21 Prover 5: Preprocessing ... % 4.16/1.21 Prover 6: Preprocessing ... % 4.16/1.21 Prover 3: Preprocessing ... % 11.06/2.14 Prover 3: Constructing countermodel ... % 11.06/2.15 Prover 1: Constructing countermodel ... % 11.50/2.16 Prover 6: Proving ... % 12.18/2.34 Prover 5: Proving ... % 12.95/2.36 Prover 2: Proving ... % 14.16/2.53 Prover 4: Constructing countermodel ... % 15.57/2.70 Prover 0: Proving ... % 18.78/3.16 Prover 3: gave up % 19.21/3.18 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 19.91/3.28 Prover 7: Preprocessing ... % 24.46/3.85 Prover 1: gave up % 24.46/3.87 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 25.17/3.95 Prover 8: Preprocessing ... % 25.17/3.96 Prover 7: Warning: ignoring some quantifiers % 25.60/4.03 Prover 7: Constructing countermodel ... % 26.57/4.12 Prover 8: Warning: ignoring some quantifiers % 26.57/4.13 Prover 8: Constructing countermodel ... % 37.62/5.57 Prover 8: gave up % 37.62/5.59 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 38.32/5.65 Prover 9: Preprocessing ... % 41.27/6.02 Prover 9: Constructing countermodel ... % 60.07/8.40 Prover 2: stopped % 60.07/8.42 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 60.75/8.48 Prover 10: Preprocessing ... % 61.25/8.55 Prover 10: Warning: ignoring some quantifiers % 61.25/8.55 Prover 10: Constructing countermodel ... % 69.68/9.67 Prover 10: Found proof (size 108) % 69.68/9.67 Prover 10: proved (1254ms) % 69.68/9.67 Prover 0: stopped % 69.68/9.67 Prover 4: stopped % 69.68/9.67 Prover 9: stopped % 69.68/9.67 Prover 7: stopped % 69.68/9.67 Prover 5: stopped % 69.68/9.67 Prover 6: stopped % 69.68/9.67 % 69.68/9.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 69.68/9.67 % 69.68/9.68 % SZS output start Proof for theBenchmark % 69.68/9.69 Assumptions after simplification: % 69.68/9.69 --------------------------------- % 69.68/9.69 % 69.68/9.69 (axiom_01) % 69.68/9.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (host(v1) = v2) | ~ (host(v0) = % 69.68/9.71 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 = v2) & s(v2) = v3 & % 69.68/9.71 $i(v3))) % 69.68/9.71 % 69.68/9.71 (axiom_13) % 69.68/9.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (m_NotNorm(v2) = % 69.68/9.71 v3) | ~ (m_Ack(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 69.68/9.71 % 69.68/9.71 (axiom_19) % 69.68/9.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (m_NotNorm(v1) = v2) | ~ % 69.68/9.71 (m_Down(v0) = v2) | ~ $i(v1) | ~ $i(v0)) % 69.68/9.71 % 69.68/9.71 (axiom_46) % 69.68/9.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 69.68/9.71 (cons(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v3) | % 69.68/9.71 elem(v0, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 69.68/9.71 (cons(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v2) | % 69.68/9.71 elem(v0, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (cons(v0, v1) % 69.68/9.71 = v2) | ~ $i(v1) | ~ $i(v0) | elem(v0, v2)) % 69.68/9.71 % 69.68/9.71 (axiom_47) % 69.68/9.72 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 69.68/9.72 (snoc(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v3) | % 69.68/9.72 elem(v0, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 69.68/9.72 (snoc(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v2) | % 69.68/9.72 elem(v0, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (snoc(v1, v0) % 69.68/9.72 = v2) | ~ $i(v1) | ~ $i(v0) | elem(v0, v2)) % 69.68/9.72 % 69.68/9.72 (conj) % 70.44/9.74 $i(down) & $i(ldr) & $i(elid) & $i(status) & $i(pendack) & $i(alive) & % 70.44/9.74 $i(norm) & $i(elec_1) & $i(elec_2) & $i(nbr_proc) & $i(zero) & ? [v0: $i] : % 70.44/9.74 ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: % 70.44/9.74 $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] % 70.44/9.74 : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : % 70.44/9.74 ? [v17: $i] : ( ~ (norm = elec_2) & index(ldr, v17) = v17 & index(status, v17) % 70.44/9.74 = norm & index(status, v4) = elec_2 & index(pendack, v4) = v15 & snoc(v1, % 70.44/9.74 v7) = v8 & cons(v6, v1) = v5 & m_NormQ(v2) = v6 & m_NotNorm(v2) = v7 & % 70.44/9.74 m_Down(v11) = v13 & s(v15) = v16 & s(zero) = v0 & m_Ack(v12, v10) = v14 & % 70.44/9.74 host(v12) = v4 & host(v11) = v16 & host(v10) = v15 & host(v9) = v17 & % 70.44/9.74 host(v3) = v4 & host(v2) = v4 & queue(v4) = v5 & $i(v17) & $i(v16) & $i(v15) % 70.44/9.74 & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) % 70.44/9.74 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 70.44/9.74 leq(nbr_proc, v16) & setIn(v12, alive) & setIn(v9, alive) & setIn(v3, alive) % 70.44/9.74 & elem(v14, v8) & elem(v13, v8) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] % 70.44/9.74 : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ( ~ % 70.44/9.74 (m_Down(v20) = v23) | ~ (m_Ack(v21, v19) = v22) | ~ (host(v18) = v24) | % 70.44/9.74 ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v21, alive) | % 70.44/9.74 ~ setIn(v18, alive) | ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? % 70.44/9.74 [v28: $i] : ? [v29: $i] : ? [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? % 70.44/9.74 [v33: $i] : (( ~ (v33 = norm) & index(status, v24) = v33 & $i(v33)) | ( ~ % 70.44/9.74 (v32 = v24) & index(ldr, v24) = v32 & $i(v32)) | (host(v21) = v25 & % 70.44/9.74 $i(v25) & (( ~ (v31 = v28) & index(pendack, v25) = v27 & s(v27) = v28 % 70.44/9.74 & host(v20) = v31 & $i(v31) & $i(v28) & $i(v27)) | ( ~ (v30 = v27) % 70.44/9.74 & index(pendack, v25) = v27 & host(v19) = v30 & $i(v30) & $i(v27)) % 70.44/9.74 | ( ~ (v29 = elec_2) & index(status, v25) = v29 & $i(v29)) | % 70.44/9.74 (index(pendack, v25) = v27 & s(v27) = v28 & $i(v28) & $i(v27) & ~ % 70.44/9.74 leq(nbr_proc, v28)) | (queue(v25) = v26 & $i(v26) & ( ~ elem(v23, % 70.44/9.74 v26) | ~ elem(v22, v26))))))) & ! [v18: $i] : ! [v19: $i] : % 70.44/9.74 ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ( % 70.44/9.74 ~ (m_Down(v20) = v22) | ~ (m_Down(v19) = v23) | ~ (host(v21) = nbr_proc) % 70.44/9.74 | ~ (host(v18) = v24) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) % 70.44/9.74 | ~ setIn(v18, alive) | ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? % 70.44/9.74 [v28: $i] : ? [v29: $i] : ? [v30: $i] : ? [v31: $i] : ($i(v31) & (( ~ % 70.44/9.74 (v31 = v26) & index(down, nbr_proc) = v25 & host(v20) = v26 & % 70.44/9.74 $i(v26) & $i(v25) & leq(v0, v31) & ~ leq(nbr_proc, v31) & ~ % 70.44/9.74 setIn(v31, v25)) | ( ~ (v29 = elec_1) & index(status, nbr_proc) = % 70.44/9.74 v29 & $i(v29)) | ( ~ (v28 = nbr_proc) & host(v19) = v28 & $i(v28)) | % 70.44/9.74 (queue(v24) = v30 & $i(v30) & ~ elem(v23, v30)) | (queue(nbr_proc) = % 70.44/9.74 v27 & $i(v27) & ~ elem(v22, v27))))) & ! [v18: $i] : ! [v19: $i] % 70.44/9.74 : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ( ~ % 70.44/9.74 (m_Down(v19) = v21) | ~ (host(v20) = v22) | ~ (host(v18) = v23) | ~ % 70.44/9.74 $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v20, alive) | ~ setIn(v18, % 70.44/9.74 alive) | ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : (( % 70.44/9.74 ~ (v27 = norm) & index(status, v23) = v27 & $i(v27)) | ( ~ (v26 = v23) % 70.44/9.74 & index(ldr, v23) = v26 & $i(v26)) | ( ~ (v25 = v23) & host(v19) = v25 % 70.44/9.74 & $i(v25)) | (queue(v22) = v24 & $i(v24) & ~ elem(v21, v24)))) & ! % 70.44/9.74 [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! % 70.44/9.74 [v23: $i] : ( ~ (m_Halt(v20) = v22) | ~ (host(v19) = v23) | ~ (host(v18) = % 70.44/9.74 v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v20, alive) | ~ % 70.44/9.74 setIn(v18, alive) | ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: % 70.44/9.74 $i] : ? [v28: $i] : ? [v29: $i] : (( ~ (v29 = norm) & index(status, % 70.44/9.74 v21) = v29 & $i(v29)) | ( ~ (v28 = v21) & index(ldr, v21) = v28 & % 70.44/9.74 $i(v28)) | ( ~ (v27 = elec_2) & index(status, v24) = v27 & host(v20) = % 70.44/9.74 v24 & $i(v27) & $i(v24)) | (index(pendack, v24) = v25 & host(v20) = % 70.44/9.74 v24 & $i(v25) & $i(v24) & leq(v25, v21)) | (queue(v23) = v26 & $i(v26) % 70.44/9.74 & ~ elem(v22, v26)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : % 70.44/9.74 ! [v21: $i] : ! [v22: $i] : ( ~ (m_Ack(v20, v18) = v21) | ~ (host(v19) = % 70.44/9.74 v22) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ? [v23: $i] : ? [v24: % 70.44/9.74 $i] : ? [v25: $i] : ((host(v20) = v25 & host(v18) = v24 & $i(v25) & % 70.44/9.74 $i(v24) & ~ leq(v24, v25)) | (queue(v22) = v23 & $i(v23) & ~ % 70.44/9.74 elem(v21, v23)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! % 70.44/9.74 [v21: $i] : ! [v22: $i] : ( ~ (m_Ack(v18, v19) = v22) | ~ (host(v20) = % 70.44/9.74 v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v20, alive) | ~ % 70.44/9.74 setIn(v18, alive) | ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: % 70.44/9.74 $i] : ? [v27: $i] : (( ~ (v26 = elec_2) & index(status, v21) = v26 & % 70.44/9.74 $i(v26)) | ( ~ (v25 = elec_2) & index(status, v24) = v25 & host(v18) = % 70.44/9.74 v24 & $i(v25) & $i(v24)) | ( ~ (v23 = v21) & host(v19) = v23 & % 70.44/9.74 $i(v23)) | (host(v18) = v24 & queue(v24) = v27 & $i(v27) & $i(v24) & % 70.44/9.74 ~ elem(v22, v27)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! % 70.44/9.74 [v21: $i] : ( ~ (m_Ldr(v19) = v20) | ~ (host(v18) = v21) | ~ $i(v19) | ~ % 70.44/9.74 $i(v18) | ? [v22: $i] : ? [v23: $i] : ((host(v19) = v23 & $i(v23) & ~ % 70.44/9.74 leq(v21, v23)) | (queue(v21) = v22 & $i(v22) & ~ elem(v20, v22)))) & % 70.44/9.74 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ (m_Down(v19) % 70.44/9.74 = v20) | ~ (host(v18) = v21) | ~ $i(v19) | ~ $i(v18) | ? [v22: $i] : % 70.44/9.74 ? [v23: $i] : (( ~ (v23 = v21) & host(v19) = v23 & $i(v23)) | (queue(v21) % 70.44/9.74 = v22 & $i(v22) & ~ elem(v20, v22)))) & ! [v18: $i] : ! [v19: $i] : % 70.44/9.74 ! [v20: $i] : ! [v21: $i] : ( ~ (m_Halt(v19) = v20) | ~ (host(v18) = v21) % 70.44/9.75 | ~ $i(v19) | ~ $i(v18) | ? [v22: $i] : ? [v23: $i] : ((host(v19) = % 70.44/9.75 v23 & $i(v23) & ~ leq(v21, v23)) | (queue(v21) = v22 & $i(v22) & ~ % 70.44/9.75 elem(v20, v22)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! % 70.44/9.75 [v21: $i] : ( ~ (host(v19) = v21) | ~ (host(v18) = v20) | ~ $i(v19) | ~ % 70.44/9.75 $i(v18) | ~ setIn(v19, alive) | ~ setIn(v18, alive) | leq(v20, v21) | ? % 70.44/9.75 [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : (( ~ (v23 = % 70.44/9.75 elec_2) & index(status, v21) = v23 & $i(v23)) | ( ~ (v22 = elec_2) & % 70.44/9.75 index(status, v20) = v22 & $i(v22)) | (index(pendack, v21) = v25 & % 70.44/9.75 index(pendack, v20) = v24 & $i(v25) & $i(v24) & ~ leq(v24, v25)))) & % 70.44/9.75 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ (host(v19) = % 70.44/9.75 v21) | ~ (host(v18) = v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, % 70.44/9.75 alive) | ~ setIn(v18, alive) | leq(v20, v21) | ? [v22: $i] : ? [v23: % 70.44/9.75 $i] : ? [v24: $i] : (( ~ (v23 = elec_2) & index(status, v21) = v23 & % 70.44/9.75 $i(v23)) | ( ~ (v22 = elec_2) & index(status, v20) = v22 & $i(v22)) | % 70.44/9.75 (index(pendack, v21) = v24 & $i(v24) & leq(v24, v20)))) & ! [v18: $i] : % 70.44/9.75 ! [v19: $i] : ! [v20: $i] : (v19 = v18 | ~ (host(v19) = v20) | ~ % 70.44/9.75 (host(v18) = v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, alive) | ~ % 70.44/9.75 setIn(v18, alive)) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ % 70.44/9.75 (m_Ack(v19, v18) = v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, alive) | % 70.44/9.75 ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : (host(v19) = % 70.44/9.75 v21 & $i(v21) & ((index(pendack, v21) = v24 & host(v18) = v23 & $i(v24) % 70.44/9.75 & $i(v23) & leq(v23, v24)) | (queue(v21) = v22 & $i(v22) & ~ % 70.44/9.75 elem(v20, v22))))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( % 70.44/9.75 ~ (m_Ack(v19, v18) = v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, alive) % 70.44/9.75 | ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : (host(v19) = v21 & $i(v21) % 70.44/9.75 & (( ~ (v22 = elec_1) & index(status, v21) = v22 & $i(v22)) | % 70.44/9.75 (queue(v21) = v23 & $i(v23) & ~ elem(v20, v23))))) & ! [v18: $i] : % 70.44/9.75 ! [v19: $i] : ( ~ (host(v18) = v19) | ~ $i(v18) | ~ setIn(v18, alive) | ? % 70.44/9.75 [v20: $i] : ? [v21: $i] : ((v21 = v18 & index(elid, v19) = v18) | ( ~ % 70.44/9.75 (v20 = elec_1) & ~ (v20 = elec_2) & index(status, v19) = v20 & % 70.44/9.75 $i(v20))))) % 70.44/9.75 % 70.44/9.75 (function-axioms) % 70.44/9.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 70.44/9.75 (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 70.44/9.75 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (snoc(v3, v2) = v1) | ~ (snoc(v3, % 70.44/9.75 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 70.44/9.75 = v0 | ~ (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) & ! [v0: $i] : ! % 70.44/9.75 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (m_Ack(v3, v2) = v1) | ~ % 70.44/9.75 (m_Ack(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 70.44/9.75 ~ (pidMsg(v2) = v1) | ~ (pidMsg(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 70.44/9.75 ! [v2: $i] : (v1 = v0 | ~ (init(v2) = v1) | ~ (init(v2) = v0)) & ! [v0: $i] % 70.44/9.75 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (last(v2) = v1) | ~ (last(v2) = % 70.44/9.75 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (tail(v2) = % 70.44/9.75 v1) | ~ (tail(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 70.44/9.75 = v0 | ~ (head(v2) = v1) | ~ (head(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 70.44/9.75 : ! [v2: $i] : (v1 = v0 | ~ (m_NormQ(v2) = v1) | ~ (m_NormQ(v2) = v0)) & ! % 70.44/9.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (m_Ldr(v2) = v1) | ~ % 70.44/9.75 (m_Ldr(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 70.44/9.75 (m_NotNorm(v2) = v1) | ~ (m_NotNorm(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 70.44/9.75 : ! [v2: $i] : (v1 = v0 | ~ (m_Down(v2) = v1) | ~ (m_Down(v2) = v0)) & ! % 70.44/9.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (m_Halt(v2) = v1) | ~ % 70.44/9.75 (m_Halt(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 70.44/9.75 (s(v2) = v1) | ~ (s(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 70.44/9.75 (v1 = v0 | ~ (host(v2) = v1) | ~ (host(v2) = v0)) & ! [v0: $i] : ! [v1: % 70.44/9.75 $i] : ! [v2: $i] : (v1 = v0 | ~ (queue(v2) = v1) | ~ (queue(v2) = v0)) % 70.44/9.75 % 70.44/9.75 Further assumptions not needed in the proof: % 70.44/9.75 -------------------------------------------- % 70.44/9.75 axiom, axiom_02, axiom_03, axiom_04, axiom_05, axiom_06, axiom_07, axiom_08, % 70.44/9.75 axiom_09, axiom_10, axiom_11, axiom_12, axiom_14, axiom_15, axiom_16, axiom_17, % 70.44/9.75 axiom_18, axiom_20, axiom_21, axiom_22, axiom_23, axiom_24, axiom_25, axiom_26, % 70.44/9.75 axiom_27, axiom_28, axiom_29, axiom_30, axiom_31, axiom_32, axiom_33, axiom_34, % 70.44/9.75 axiom_35, axiom_36, axiom_37, axiom_38, axiom_39, axiom_40, axiom_41, axiom_42, % 70.44/9.75 axiom_43, axiom_44, axiom_45, axiom_48, axiom_49, axiom_50, axiom_51, axiom_52, % 70.44/9.75 axiom_53, axiom_54, axiom_55, axiom_56, axiom_57, axiom_58, axiom_59, axiom_60, % 70.44/9.75 axiom_61, axiom_62, axiom_63, axiom_64, axiom_65 % 70.44/9.75 % 70.44/9.75 Those formulas are unsatisfiable: % 70.44/9.75 --------------------------------- % 70.44/9.75 % 70.44/9.75 Begin of proof % 70.44/9.75 | % 70.44/9.75 | ALPHA: (axiom_46) implies: % 70.44/9.75 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (cons(v1, % 70.44/9.75 | v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, v2) | % 70.44/9.75 | elem(v0, v3)) % 70.44/9.75 | % 70.44/9.75 | ALPHA: (axiom_47) implies: % 70.44/9.75 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 70.44/9.75 | (snoc(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ elem(v0, % 70.44/9.75 | v3) | elem(v0, v2)) % 70.44/9.75 | % 70.44/9.75 | ALPHA: (conj) implies: % 70.44/9.77 | (3) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 70.44/9.77 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 70.44/9.77 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 70.44/9.77 | ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ( ~ (norm = elec_2) & % 70.44/9.77 | index(ldr, v17) = v17 & index(status, v17) = norm & index(status, v4) % 70.44/9.77 | = elec_2 & index(pendack, v4) = v15 & snoc(v1, v7) = v8 & cons(v6, % 70.44/9.77 | v1) = v5 & m_NormQ(v2) = v6 & m_NotNorm(v2) = v7 & m_Down(v11) = % 70.44/9.77 | v13 & s(v15) = v16 & s(zero) = v0 & m_Ack(v12, v10) = v14 & host(v12) % 70.44/9.77 | = v4 & host(v11) = v16 & host(v10) = v15 & host(v9) = v17 & host(v3) % 70.44/9.77 | = v4 & host(v2) = v4 & queue(v4) = v5 & $i(v17) & $i(v16) & $i(v15) & % 70.44/9.77 | $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & % 70.44/9.77 | $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) % 70.44/9.77 | & leq(nbr_proc, v16) & setIn(v12, alive) & setIn(v9, alive) & % 70.44/9.77 | setIn(v3, alive) & elem(v14, v8) & elem(v13, v8) & ! [v18: $i] : ! % 70.44/9.77 | [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] % 70.44/9.77 | : ! [v24: $i] : ( ~ (m_Down(v20) = v23) | ~ (m_Ack(v21, v19) = v22) % 70.44/9.77 | | ~ (host(v18) = v24) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ % 70.44/9.77 | $i(v18) | ~ setIn(v21, alive) | ~ setIn(v18, alive) | ? [v25: % 70.44/9.77 | $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? [v29: $i] : % 70.44/9.77 | ? [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? [v33: $i] : (( ~ % 70.44/9.77 | (v33 = norm) & index(status, v24) = v33 & $i(v33)) | ( ~ (v32 = % 70.44/9.77 | v24) & index(ldr, v24) = v32 & $i(v32)) | (host(v21) = v25 & % 70.44/9.77 | $i(v25) & (( ~ (v31 = v28) & index(pendack, v25) = v27 & s(v27) % 70.44/9.77 | = v28 & host(v20) = v31 & $i(v31) & $i(v28) & $i(v27)) | ( % 70.44/9.77 | ~ (v30 = v27) & index(pendack, v25) = v27 & host(v19) = v30 % 70.44/9.77 | & $i(v30) & $i(v27)) | ( ~ (v29 = elec_2) & index(status, % 70.44/9.77 | v25) = v29 & $i(v29)) | (index(pendack, v25) = v27 & % 70.44/9.77 | s(v27) = v28 & $i(v28) & $i(v27) & ~ leq(nbr_proc, v28)) | % 70.44/9.77 | (queue(v25) = v26 & $i(v26) & ( ~ elem(v23, v26) | ~ % 70.44/9.77 | elem(v22, v26))))))) & ! [v18: $i] : ! [v19: $i] : ! % 70.44/9.77 | [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: $i] % 70.44/9.77 | : ( ~ (m_Down(v20) = v22) | ~ (m_Down(v19) = v23) | ~ (host(v21) = % 70.44/9.77 | nbr_proc) | ~ (host(v18) = v24) | ~ $i(v21) | ~ $i(v20) | ~ % 70.44/9.77 | $i(v19) | ~ $i(v18) | ~ setIn(v18, alive) | ? [v25: $i] : ? % 70.44/9.77 | [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? [v29: $i] : ? [v30: % 70.44/9.77 | $i] : ? [v31: $i] : ($i(v31) & (( ~ (v31 = v26) & index(down, % 70.44/9.77 | nbr_proc) = v25 & host(v20) = v26 & $i(v26) & $i(v25) & % 70.44/9.77 | leq(v0, v31) & ~ leq(nbr_proc, v31) & ~ setIn(v31, v25)) | % 70.44/9.77 | ( ~ (v29 = elec_1) & index(status, nbr_proc) = v29 & $i(v29)) | % 70.44/9.77 | ( ~ (v28 = nbr_proc) & host(v19) = v28 & $i(v28)) | (queue(v24) % 70.44/9.77 | = v30 & $i(v30) & ~ elem(v23, v30)) | (queue(nbr_proc) = v27 % 70.44/9.77 | & $i(v27) & ~ elem(v22, v27))))) & ! [v18: $i] : ! [v19: % 70.44/9.77 | $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ( % 70.44/9.77 | ~ (m_Down(v19) = v21) | ~ (host(v20) = v22) | ~ (host(v18) = v23) % 70.44/9.77 | | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v20, alive) | ~ % 70.44/9.77 | setIn(v18, alive) | ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? % 70.44/9.77 | [v27: $i] : (( ~ (v27 = norm) & index(status, v23) = v27 & $i(v27)) % 70.44/9.77 | | ( ~ (v26 = v23) & index(ldr, v23) = v26 & $i(v26)) | ( ~ (v25 = % 70.44/9.77 | v23) & host(v19) = v25 & $i(v25)) | (queue(v22) = v24 & % 70.44/9.77 | $i(v24) & ~ elem(v21, v24)))) & ! [v18: $i] : ! [v19: $i] : % 70.44/9.77 | ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ( ~ % 70.44/9.77 | (m_Halt(v20) = v22) | ~ (host(v19) = v23) | ~ (host(v18) = v21) | % 70.44/9.77 | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v20, alive) | ~ % 70.44/9.77 | setIn(v18, alive) | ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? % 70.44/9.77 | [v27: $i] : ? [v28: $i] : ? [v29: $i] : (( ~ (v29 = norm) & % 70.44/9.77 | index(status, v21) = v29 & $i(v29)) | ( ~ (v28 = v21) & % 70.44/9.77 | index(ldr, v21) = v28 & $i(v28)) | ( ~ (v27 = elec_2) & % 70.44/9.77 | index(status, v24) = v27 & host(v20) = v24 & $i(v27) & $i(v24)) % 70.44/9.77 | | (index(pendack, v24) = v25 & host(v20) = v24 & $i(v25) & % 70.44/9.77 | $i(v24) & leq(v25, v21)) | (queue(v23) = v26 & $i(v26) & ~ % 70.44/9.77 | elem(v22, v26)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] % 70.44/9.78 | : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Ack(v20, v18) = v21) | ~ % 70.44/9.78 | (host(v19) = v22) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ? [v23: % 70.44/9.78 | $i] : ? [v24: $i] : ? [v25: $i] : ((host(v20) = v25 & host(v18) % 70.44/9.78 | = v24 & $i(v25) & $i(v24) & ~ leq(v24, v25)) | (queue(v22) = % 70.44/9.78 | v23 & $i(v23) & ~ elem(v21, v23)))) & ! [v18: $i] : ! [v19: % 70.44/9.78 | $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ( ~ (m_Ack(v18, % 70.44/9.78 | v19) = v22) | ~ (host(v20) = v21) | ~ $i(v20) | ~ $i(v19) | % 70.44/9.78 | ~ $i(v18) | ~ setIn(v20, alive) | ~ setIn(v18, alive) | ? [v23: % 70.44/9.78 | $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : % 70.44/9.78 | (( ~ (v26 = elec_2) & index(status, v21) = v26 & $i(v26)) | ( ~ % 70.44/9.78 | (v25 = elec_2) & index(status, v24) = v25 & host(v18) = v24 & % 70.44/9.78 | $i(v25) & $i(v24)) | ( ~ (v23 = v21) & host(v19) = v23 & % 70.44/9.78 | $i(v23)) | (host(v18) = v24 & queue(v24) = v27 & $i(v27) & % 70.44/9.78 | $i(v24) & ~ elem(v22, v27)))) & ! [v18: $i] : ! [v19: $i] : % 70.44/9.78 | ! [v20: $i] : ! [v21: $i] : ( ~ (m_Ldr(v19) = v20) | ~ (host(v18) = % 70.44/9.78 | v21) | ~ $i(v19) | ~ $i(v18) | ? [v22: $i] : ? [v23: $i] : % 70.44/9.78 | ((host(v19) = v23 & $i(v23) & ~ leq(v21, v23)) | (queue(v21) = v22 % 70.44/9.78 | & $i(v22) & ~ elem(v20, v22)))) & ! [v18: $i] : ! [v19: $i] % 70.44/9.78 | : ! [v20: $i] : ! [v21: $i] : ( ~ (m_Down(v19) = v20) | ~ % 70.44/9.78 | (host(v18) = v21) | ~ $i(v19) | ~ $i(v18) | ? [v22: $i] : ? % 70.44/9.78 | [v23: $i] : (( ~ (v23 = v21) & host(v19) = v23 & $i(v23)) | % 70.44/9.78 | (queue(v21) = v22 & $i(v22) & ~ elem(v20, v22)))) & ! [v18: $i] % 70.44/9.78 | : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ (m_Halt(v19) = % 70.44/9.78 | v20) | ~ (host(v18) = v21) | ~ $i(v19) | ~ $i(v18) | ? [v22: % 70.44/9.78 | $i] : ? [v23: $i] : ((host(v19) = v23 & $i(v23) & ~ leq(v21, % 70.44/9.78 | v23)) | (queue(v21) = v22 & $i(v22) & ~ elem(v20, v22)))) & % 70.44/9.78 | ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ % 70.44/9.78 | (host(v19) = v21) | ~ (host(v18) = v20) | ~ $i(v19) | ~ $i(v18) % 70.44/9.78 | | ~ setIn(v19, alive) | ~ setIn(v18, alive) | leq(v20, v21) | ? % 70.44/9.78 | [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? [v25: $i] : (( ~ (v23 % 70.44/9.78 | = elec_2) & index(status, v21) = v23 & $i(v23)) | ( ~ (v22 = % 70.44/9.78 | elec_2) & index(status, v20) = v22 & $i(v22)) | % 70.44/9.78 | (index(pendack, v21) = v25 & index(pendack, v20) = v24 & $i(v25) % 70.44/9.78 | & $i(v24) & ~ leq(v24, v25)))) & ! [v18: $i] : ! [v19: $i] : % 70.44/9.78 | ! [v20: $i] : ! [v21: $i] : ( ~ (host(v19) = v21) | ~ (host(v18) = % 70.44/9.78 | v20) | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, alive) | ~ % 70.44/9.78 | setIn(v18, alive) | leq(v20, v21) | ? [v22: $i] : ? [v23: $i] : % 70.44/9.78 | ? [v24: $i] : (( ~ (v23 = elec_2) & index(status, v21) = v23 & % 70.44/9.78 | $i(v23)) | ( ~ (v22 = elec_2) & index(status, v20) = v22 & % 70.44/9.78 | $i(v22)) | (index(pendack, v21) = v24 & $i(v24) & leq(v24, % 70.44/9.78 | v20)))) & ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : (v19 = % 70.44/9.78 | v18 | ~ (host(v19) = v20) | ~ (host(v18) = v20) | ~ $i(v19) | ~ % 70.44/9.78 | $i(v18) | ~ setIn(v19, alive) | ~ setIn(v18, alive)) & ! [v18: % 70.44/9.78 | $i] : ! [v19: $i] : ! [v20: $i] : ( ~ (m_Ack(v19, v18) = v20) | % 70.44/9.78 | ~ $i(v19) | ~ $i(v18) | ~ setIn(v19, alive) | ? [v21: $i] : ? % 70.44/9.78 | [v22: $i] : ? [v23: $i] : ? [v24: $i] : (host(v19) = v21 & % 70.44/9.78 | $i(v21) & ((index(pendack, v21) = v24 & host(v18) = v23 & $i(v24) % 70.44/9.78 | & $i(v23) & leq(v23, v24)) | (queue(v21) = v22 & $i(v22) & ~ % 70.44/9.78 | elem(v20, v22))))) & ! [v18: $i] : ! [v19: $i] : ! [v20: % 70.44/9.78 | $i] : ( ~ (m_Ack(v19, v18) = v20) | ~ $i(v19) | ~ $i(v18) | ~ % 70.44/9.78 | setIn(v19, alive) | ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : % 70.44/9.78 | (host(v19) = v21 & $i(v21) & (( ~ (v22 = elec_1) & index(status, % 70.44/9.78 | v21) = v22 & $i(v22)) | (queue(v21) = v23 & $i(v23) & ~ % 70.44/9.78 | elem(v20, v23))))) & ! [v18: $i] : ! [v19: $i] : ( ~ % 70.44/9.78 | (host(v18) = v19) | ~ $i(v18) | ~ setIn(v18, alive) | ? [v20: % 70.44/9.78 | $i] : ? [v21: $i] : ((v21 = v18 & index(elid, v19) = v18) | ( ~ % 70.44/9.78 | (v20 = elec_1) & ~ (v20 = elec_2) & index(status, v19) = v20 & % 70.44/9.78 | $i(v20))))) % 70.44/9.78 | % 70.44/9.78 | ALPHA: (function-axioms) implies: % 70.44/9.78 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (queue(v2) = % 70.44/9.78 | v1) | ~ (queue(v2) = v0)) % 70.44/9.78 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (host(v2) = v1) % 70.44/9.78 | | ~ (host(v2) = v0)) % 70.44/9.78 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | % 70.44/9.78 | ~ (s(v2) = v0)) % 70.44/9.78 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 70.44/9.78 | (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) % 70.44/9.78 | % 70.44/9.78 | DELTA: instantiating (3) with fresh symbols all_65_0, all_65_1, all_65_2, % 70.44/9.78 | all_65_3, all_65_4, all_65_5, all_65_6, all_65_7, all_65_8, all_65_9, % 70.44/9.78 | all_65_10, all_65_11, all_65_12, all_65_13, all_65_14, all_65_15, % 70.44/9.78 | all_65_16, all_65_17 gives: % 70.44/9.79 | (8) ~ (norm = elec_2) & index(ldr, all_65_0) = all_65_0 & index(status, % 70.44/9.79 | all_65_0) = norm & index(status, all_65_13) = elec_2 & index(pendack, % 70.44/9.79 | all_65_13) = all_65_2 & snoc(all_65_16, all_65_10) = all_65_9 & % 70.44/9.79 | cons(all_65_11, all_65_16) = all_65_12 & m_NormQ(all_65_15) = all_65_11 % 70.44/9.79 | & m_NotNorm(all_65_15) = all_65_10 & m_Down(all_65_6) = all_65_4 & % 70.44/9.79 | s(all_65_2) = all_65_1 & s(zero) = all_65_17 & m_Ack(all_65_5, % 70.44/9.79 | all_65_7) = all_65_3 & host(all_65_5) = all_65_13 & host(all_65_6) = % 70.44/9.79 | all_65_1 & host(all_65_7) = all_65_2 & host(all_65_8) = all_65_0 & % 70.44/9.79 | host(all_65_14) = all_65_13 & host(all_65_15) = all_65_13 & % 70.44/9.79 | queue(all_65_13) = all_65_12 & $i(all_65_0) & $i(all_65_1) & % 70.44/9.79 | $i(all_65_2) & $i(all_65_3) & $i(all_65_4) & $i(all_65_5) & % 70.44/9.79 | $i(all_65_6) & $i(all_65_7) & $i(all_65_8) & $i(all_65_9) & % 70.44/9.79 | $i(all_65_10) & $i(all_65_11) & $i(all_65_12) & $i(all_65_13) & % 70.44/9.79 | $i(all_65_14) & $i(all_65_15) & $i(all_65_16) & $i(all_65_17) & % 70.44/9.79 | leq(nbr_proc, all_65_1) & setIn(all_65_5, alive) & setIn(all_65_8, % 70.44/9.79 | alive) & setIn(all_65_14, alive) & elem(all_65_3, all_65_9) & % 70.44/9.79 | elem(all_65_4, all_65_9) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 70.44/9.79 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ (m_Down(v2) = % 70.44/9.79 | v5) | ~ (m_Ack(v3, v1) = v4) | ~ (host(v0) = v6) | ~ $i(v3) | ~ % 70.44/9.79 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v3, alive) | ~ setIn(v0, % 70.44/9.79 | alive) | ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : % 70.44/9.79 | ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: % 70.44/9.79 | $i] : (( ~ (v15 = norm) & index(status, v6) = v15 & $i(v15)) | ( ~ % 70.44/9.79 | (v14 = v6) & index(ldr, v6) = v14 & $i(v14)) | (host(v3) = v7 & % 70.44/9.79 | $i(v7) & (( ~ (v13 = v10) & index(pendack, v7) = v9 & s(v9) = v10 % 70.44/9.79 | & host(v2) = v13 & $i(v13) & $i(v10) & $i(v9)) | ( ~ (v12 = % 70.44/9.79 | v9) & index(pendack, v7) = v9 & host(v1) = v12 & $i(v12) & % 70.44/9.79 | $i(v9)) | ( ~ (v11 = elec_2) & index(status, v7) = v11 & % 70.44/9.79 | $i(v11)) | (index(pendack, v7) = v9 & s(v9) = v10 & $i(v10) & % 70.44/9.79 | $i(v9) & ~ leq(nbr_proc, v10)) | (queue(v7) = v8 & $i(v8) & % 70.44/9.79 | ( ~ elem(v5, v8) | ~ elem(v4, v8))))))) & ! [v0: $i] : ! % 70.44/9.79 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! % 70.44/9.79 | [v6: $i] : ( ~ (m_Down(v2) = v4) | ~ (m_Down(v1) = v5) | ~ (host(v3) % 70.44/9.79 | = nbr_proc) | ~ (host(v0) = v6) | ~ $i(v3) | ~ $i(v2) | ~ % 70.44/9.79 | $i(v1) | ~ $i(v0) | ~ setIn(v0, alive) | ? [v7: $i] : ? [v8: $i] % 70.44/9.79 | : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: % 70.44/9.79 | $i] : ($i(v13) & (( ~ (v13 = v8) & index(down, nbr_proc) = v7 & % 70.44/9.79 | host(v2) = v8 & $i(v8) & $i(v7) & leq(all_65_17, v13) & ~ % 70.44/9.79 | leq(nbr_proc, v13) & ~ setIn(v13, v7)) | ( ~ (v11 = elec_1) & % 70.44/9.79 | index(status, nbr_proc) = v11 & $i(v11)) | ( ~ (v10 = nbr_proc) % 70.44/9.79 | & host(v1) = v10 & $i(v10)) | (queue(v6) = v12 & $i(v12) & ~ % 70.44/9.79 | elem(v5, v12)) | (queue(nbr_proc) = v9 & $i(v9) & ~ elem(v4, % 70.44/9.79 | v9))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 70.44/9.80 | $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (m_Down(v1) = v3) | ~ % 70.44/9.80 | (host(v2) = v4) | ~ (host(v0) = v5) | ~ $i(v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v6: $i] : ? % 70.44/9.80 | [v7: $i] : ? [v8: $i] : ? [v9: $i] : (( ~ (v9 = norm) & % 70.44/9.80 | index(status, v5) = v9 & $i(v9)) | ( ~ (v8 = v5) & index(ldr, v5) % 70.44/9.80 | = v8 & $i(v8)) | ( ~ (v7 = v5) & host(v1) = v7 & $i(v7)) | % 70.44/9.80 | (queue(v4) = v6 & $i(v6) & ~ elem(v3, v6)))) & ! [v0: $i] : ! % 70.44/9.80 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 70.44/9.80 | (m_Halt(v2) = v4) | ~ (host(v1) = v5) | ~ (host(v0) = v3) | ~ % 70.44/9.80 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, % 70.44/9.80 | alive) | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 70.44/9.80 | [v10: $i] : ? [v11: $i] : (( ~ (v11 = norm) & index(status, v3) = % 70.44/9.80 | v11 & $i(v11)) | ( ~ (v10 = v3) & index(ldr, v3) = v10 & $i(v10)) % 70.44/9.80 | | ( ~ (v9 = elec_2) & index(status, v6) = v9 & host(v2) = v6 & % 70.44/9.80 | $i(v9) & $i(v6)) | (index(pendack, v6) = v7 & host(v2) = v6 & % 70.44/9.80 | $i(v7) & $i(v6) & leq(v7, v3)) | (queue(v5) = v8 & $i(v8) & ~ % 70.44/9.80 | elem(v4, v8)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 70.44/9.80 | [v3: $i] : ! [v4: $i] : ( ~ (m_Ack(v2, v0) = v3) | ~ (host(v1) = v4) % 70.44/9.80 | | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? % 70.44/9.80 | [v7: $i] : ((host(v2) = v7 & host(v0) = v6 & $i(v7) & $i(v6) & ~ % 70.44/9.80 | leq(v6, v7)) | (queue(v4) = v5 & $i(v5) & ~ elem(v3, v5)))) & ! % 70.44/9.80 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 70.44/9.80 | (m_Ack(v0, v1) = v4) | ~ (host(v2) = v3) | ~ $i(v2) | ~ $i(v1) | % 70.44/9.80 | ~ $i(v0) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v5: $i] : % 70.44/9.80 | ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : (( ~ (v8 = % 70.44/9.80 | elec_2) & index(status, v3) = v8 & $i(v8)) | ( ~ (v7 = elec_2) % 70.44/9.80 | & index(status, v6) = v7 & host(v0) = v6 & $i(v7) & $i(v6)) | ( ~ % 70.44/9.80 | (v5 = v3) & host(v1) = v5 & $i(v5)) | (host(v0) = v6 & queue(v6) % 70.44/9.80 | = v9 & $i(v9) & $i(v6) & ~ elem(v4, v9)))) & ! [v0: $i] : ! % 70.44/9.80 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (m_Ldr(v1) = v2) | ~ % 70.44/9.80 | (host(v0) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : % 70.44/9.80 | ((host(v1) = v5 & $i(v5) & ~ leq(v3, v5)) | (queue(v3) = v4 & $i(v4) % 70.44/9.80 | & ~ elem(v2, v4)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 70.44/9.80 | ! [v3: $i] : ( ~ (m_Down(v1) = v2) | ~ (host(v0) = v3) | ~ $i(v1) | % 70.44/9.80 | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (( ~ (v5 = v3) & host(v1) = v5 % 70.44/9.80 | & $i(v5)) | (queue(v3) = v4 & $i(v4) & ~ elem(v2, v4)))) & ! % 70.44/9.80 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (m_Halt(v1) = % 70.44/9.80 | v2) | ~ (host(v0) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? % 70.44/9.80 | [v5: $i] : ((host(v1) = v5 & $i(v5) & ~ leq(v3, v5)) | (queue(v3) = % 70.44/9.80 | v4 & $i(v4) & ~ elem(v2, v4)))) & ! [v0: $i] : ! [v1: $i] : ! % 70.44/9.80 | [v2: $i] : ! [v3: $i] : ( ~ (host(v1) = v3) | ~ (host(v0) = v2) | ~ % 70.44/9.80 | $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ~ setIn(v0, alive) | % 70.44/9.80 | leq(v2, v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 70.44/9.80 | (( ~ (v5 = elec_2) & index(status, v3) = v5 & $i(v5)) | ( ~ (v4 = % 70.44/9.80 | elec_2) & index(status, v2) = v4 & $i(v4)) | (index(pendack, % 70.44/9.80 | v3) = v7 & index(pendack, v2) = v6 & $i(v7) & $i(v6) & ~ % 70.44/9.80 | leq(v6, v7)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 70.44/9.80 | [v3: $i] : ( ~ (host(v1) = v3) | ~ (host(v0) = v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v1, alive) | ~ setIn(v0, alive) | leq(v2, v3) | ? % 70.44/9.80 | [v4: $i] : ? [v5: $i] : ? [v6: $i] : (( ~ (v5 = elec_2) & % 70.44/9.80 | index(status, v3) = v5 & $i(v5)) | ( ~ (v4 = elec_2) & % 70.44/9.80 | index(status, v2) = v4 & $i(v4)) | (index(pendack, v3) = v6 & % 70.44/9.80 | $i(v6) & leq(v6, v2)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 70.44/9.80 | : (v1 = v0 | ~ (host(v1) = v2) | ~ (host(v0) = v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v1, alive) | ~ setIn(v0, alive)) & ! [v0: $i] : % 70.44/9.80 | ! [v1: $i] : ! [v2: $i] : ( ~ (m_Ack(v1, v0) = v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v1, alive) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 70.44/9.80 | $i] : ? [v6: $i] : (host(v1) = v3 & $i(v3) & ((index(pendack, v3) % 70.44/9.80 | = v6 & host(v0) = v5 & $i(v6) & $i(v5) & leq(v5, v6)) | % 70.44/9.80 | (queue(v3) = v4 & $i(v4) & ~ elem(v2, v4))))) & ! [v0: $i] : ! % 70.44/9.80 | [v1: $i] : ! [v2: $i] : ( ~ (m_Ack(v1, v0) = v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v1, alive) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 70.44/9.80 | $i] : (host(v1) = v3 & $i(v3) & (( ~ (v4 = elec_1) & index(status, % 70.44/9.80 | v3) = v4 & $i(v4)) | (queue(v3) = v5 & $i(v5) & ~ elem(v2, % 70.44/9.80 | v5))))) & ! [v0: $i] : ! [v1: $i] : ( ~ (host(v0) = v1) | % 70.44/9.80 | ~ $i(v0) | ~ setIn(v0, alive) | ? [v2: $i] : ? [v3: $i] : ((v3 = % 70.44/9.80 | v0 & index(elid, v1) = v0) | ( ~ (v2 = elec_1) & ~ (v2 = elec_2) % 70.44/9.80 | & index(status, v1) = v2 & $i(v2)))) % 70.44/9.80 | % 70.44/9.80 | ALPHA: (8) implies: % 70.44/9.80 | (9) elem(all_65_4, all_65_9) % 70.44/9.80 | (10) elem(all_65_3, all_65_9) % 70.44/9.80 | (11) setIn(all_65_14, alive) % 70.44/9.80 | (12) setIn(all_65_8, alive) % 70.44/9.80 | (13) setIn(all_65_5, alive) % 70.44/9.80 | (14) leq(nbr_proc, all_65_1) % 70.44/9.80 | (15) $i(all_65_16) % 70.44/9.80 | (16) $i(all_65_15) % 70.44/9.80 | (17) $i(all_65_14) % 70.44/9.80 | (18) $i(all_65_11) % 70.44/9.80 | (19) $i(all_65_10) % 70.44/9.80 | (20) $i(all_65_8) % 70.44/9.80 | (21) $i(all_65_7) % 70.44/9.80 | (22) $i(all_65_6) % 70.44/9.80 | (23) $i(all_65_5) % 70.44/9.80 | (24) $i(all_65_4) % 70.44/9.80 | (25) $i(all_65_3) % 70.44/9.80 | (26) queue(all_65_13) = all_65_12 % 70.44/9.80 | (27) host(all_65_14) = all_65_13 % 70.44/9.80 | (28) host(all_65_8) = all_65_0 % 70.44/9.80 | (29) host(all_65_7) = all_65_2 % 70.44/9.80 | (30) host(all_65_6) = all_65_1 % 70.44/9.80 | (31) host(all_65_5) = all_65_13 % 70.44/9.80 | (32) m_Ack(all_65_5, all_65_7) = all_65_3 % 70.44/9.80 | (33) s(all_65_2) = all_65_1 % 70.44/9.80 | (34) m_Down(all_65_6) = all_65_4 % 70.44/9.80 | (35) m_NotNorm(all_65_15) = all_65_10 % 70.44/9.80 | (36) cons(all_65_11, all_65_16) = all_65_12 % 70.44/9.80 | (37) snoc(all_65_16, all_65_10) = all_65_9 % 70.44/9.80 | (38) index(pendack, all_65_13) = all_65_2 % 70.44/9.80 | (39) index(status, all_65_13) = elec_2 % 70.44/9.80 | (40) index(status, all_65_0) = norm % 70.44/9.80 | (41) index(ldr, all_65_0) = all_65_0 % 70.44/9.80 | (42) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (m_Ack(v1, v0) = v2) | % 70.44/9.80 | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ? [v3: $i] : ? [v4: % 70.44/9.80 | $i] : ? [v5: $i] : (host(v1) = v3 & $i(v3) & (( ~ (v4 = elec_1) & % 70.44/9.80 | index(status, v3) = v4 & $i(v4)) | (queue(v3) = v5 & $i(v5) & % 70.44/9.80 | ~ elem(v2, v5))))) % 70.44/9.80 | (43) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (m_Ack(v1, v0) = v2) | % 70.44/9.80 | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, alive) | ? [v3: $i] : ? [v4: % 70.44/9.80 | $i] : ? [v5: $i] : ? [v6: $i] : (host(v1) = v3 & $i(v3) & % 70.44/9.80 | ((index(pendack, v3) = v6 & host(v0) = v5 & $i(v6) & $i(v5) & % 70.44/9.80 | leq(v5, v6)) | (queue(v3) = v4 & $i(v4) & ~ elem(v2, v4))))) % 70.44/9.80 | (44) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (host(v1) = % 70.44/9.80 | v2) | ~ (host(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ setIn(v1, % 70.44/9.80 | alive) | ~ setIn(v0, alive)) % 70.44/9.80 | (45) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 70.44/9.80 | ! [v5: $i] : ! [v6: $i] : ( ~ (m_Down(v2) = v5) | ~ (m_Ack(v3, v1) = % 70.44/9.80 | v4) | ~ (host(v0) = v6) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 70.44/9.80 | $i(v0) | ~ setIn(v3, alive) | ~ setIn(v0, alive) | ? [v7: $i] : % 70.44/9.80 | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: % 70.44/9.80 | $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : (( ~ (v15 = % 70.44/9.80 | norm) & index(status, v6) = v15 & $i(v15)) | ( ~ (v14 = v6) & % 70.44/9.80 | index(ldr, v6) = v14 & $i(v14)) | (host(v3) = v7 & $i(v7) & (( ~ % 70.44/9.80 | (v13 = v10) & index(pendack, v7) = v9 & s(v9) = v10 & % 70.44/9.80 | host(v2) = v13 & $i(v13) & $i(v10) & $i(v9)) | ( ~ (v12 = % 70.44/9.80 | v9) & index(pendack, v7) = v9 & host(v1) = v12 & $i(v12) & % 70.44/9.80 | $i(v9)) | ( ~ (v11 = elec_2) & index(status, v7) = v11 & % 70.44/9.81 | $i(v11)) | (index(pendack, v7) = v9 & s(v9) = v10 & $i(v10) % 70.44/9.81 | & $i(v9) & ~ leq(nbr_proc, v10)) | (queue(v7) = v8 & $i(v8) % 70.44/9.81 | & ( ~ elem(v5, v8) | ~ elem(v4, v8))))))) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (axiom_01) with all_65_7, all_65_7, all_65_2, % 70.44/9.81 | simplifying with (21), (29) gives: % 70.44/9.81 | (46) ? [v0: any] : ( ~ (v0 = all_65_2) & s(all_65_2) = v0 & $i(v0)) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (44) with all_65_14, all_65_5, all_65_13, % 70.44/9.81 | simplifying with (11), (13), (17), (23), (27), (31) gives: % 70.44/9.81 | (47) all_65_5 = all_65_14 % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (43) with all_65_7, all_65_5, all_65_3, simplifying % 70.44/9.81 | with (13), (21), (23), (32) gives: % 70.44/9.81 | (48) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 70.44/9.81 | (host(all_65_5) = v0 & $i(v0) & ((index(pendack, v0) = v3 & % 70.44/9.81 | host(all_65_7) = v2 & $i(v3) & $i(v2) & leq(v2, v3)) | % 70.44/9.81 | (queue(v0) = v1 & $i(v1) & ~ elem(all_65_3, v1)))) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (42) with all_65_7, all_65_5, all_65_3, simplifying % 70.44/9.81 | with (13), (21), (23), (32) gives: % 70.44/9.81 | (49) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (host(all_65_5) = v0 & % 70.44/9.81 | $i(v0) & (( ~ (v1 = elec_1) & index(status, v0) = v1 & $i(v1)) | % 70.44/9.81 | (queue(v0) = v2 & $i(v2) & ~ elem(all_65_3, v2)))) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (45) with all_65_8, all_65_7, all_65_6, all_65_5, % 70.44/9.81 | all_65_3, all_65_4, all_65_0, simplifying with (12), (13), (20), % 70.44/9.81 | (21), (22), (23), (28), (32), (34) gives: % 70.44/9.81 | (50) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 70.44/9.81 | ? [v5: $i] : ? [v6: $i] : ? [v7: any] : ? [v8: $i] : (( ~ (v8 = % 70.44/9.81 | norm) & index(status, all_65_0) = v8 & $i(v8)) | ( ~ (v7 = % 70.44/9.81 | all_65_0) & index(ldr, all_65_0) = v7 & $i(v7)) | % 70.44/9.81 | (host(all_65_5) = v0 & $i(v0) & (( ~ (v6 = v3) & index(pendack, v0) % 70.44/9.81 | = v2 & s(v2) = v3 & host(all_65_6) = v6 & $i(v6) & $i(v3) & % 70.44/9.81 | $i(v2)) | ( ~ (v5 = v2) & index(pendack, v0) = v2 & % 70.44/9.81 | host(all_65_7) = v5 & $i(v5) & $i(v2)) | ( ~ (v4 = elec_2) & % 70.44/9.81 | index(status, v0) = v4 & $i(v4)) | (index(pendack, v0) = v2 & % 70.44/9.81 | s(v2) = v3 & $i(v3) & $i(v2) & ~ leq(nbr_proc, v3)) | % 70.44/9.81 | (queue(v0) = v1 & $i(v1) & ( ~ elem(all_65_3, v1) | ~ % 70.44/9.81 | elem(all_65_4, v1)))))) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (2) with all_65_3, all_65_10, all_65_16, all_65_9, % 70.44/9.81 | simplifying with (10), (15), (19), (25), (37) gives: % 70.44/9.81 | (51) all_65_3 = all_65_10 | elem(all_65_3, all_65_16) % 70.44/9.81 | % 70.44/9.81 | GROUND_INST: instantiating (2) with all_65_4, all_65_10, all_65_16, all_65_9, % 70.44/9.81 | simplifying with (9), (15), (19), (24), (37) gives: % 70.44/9.81 | (52) all_65_4 = all_65_10 | elem(all_65_4, all_65_16) % 70.44/9.81 | % 70.44/9.81 | DELTA: instantiating (46) with fresh symbol all_82_0 gives: % 70.44/9.81 | (53) ~ (all_82_0 = all_65_2) & s(all_65_2) = all_82_0 & $i(all_82_0) % 70.44/9.81 | % 70.44/9.81 | ALPHA: (53) implies: % 70.44/9.81 | (54) s(all_65_2) = all_82_0 % 70.44/9.81 | % 70.44/9.81 | DELTA: instantiating (49) with fresh symbols all_96_0, all_96_1, all_96_2 % 70.44/9.81 | gives: % 70.44/9.81 | (55) host(all_65_5) = all_96_2 & $i(all_96_2) & (( ~ (all_96_1 = elec_1) & % 70.44/9.81 | index(status, all_96_2) = all_96_1 & $i(all_96_1)) | % 70.44/9.81 | (queue(all_96_2) = all_96_0 & $i(all_96_0) & ~ elem(all_65_3, % 70.44/9.81 | all_96_0))) % 70.44/9.81 | % 70.44/9.81 | ALPHA: (55) implies: % 70.44/9.81 | (56) host(all_65_5) = all_96_2 % 70.44/9.81 | % 70.44/9.81 | DELTA: instantiating (48) with fresh symbols all_99_0, all_99_1, all_99_2, % 70.44/9.81 | all_99_3 gives: % 70.44/9.81 | (57) host(all_65_5) = all_99_3 & $i(all_99_3) & ((index(pendack, all_99_3) % 70.44/9.81 | = all_99_0 & host(all_65_7) = all_99_1 & $i(all_99_0) & % 70.44/9.81 | $i(all_99_1) & leq(all_99_1, all_99_0)) | (queue(all_99_3) = % 70.44/9.81 | all_99_2 & $i(all_99_2) & ~ elem(all_65_3, all_99_2))) % 70.44/9.81 | % 70.44/9.81 | ALPHA: (57) implies: % 70.44/9.81 | (58) host(all_65_5) = all_99_3 % 70.44/9.81 | % 70.44/9.81 | DELTA: instantiating (50) with fresh symbols all_107_0, all_107_1, all_107_2, % 70.44/9.81 | all_107_3, all_107_4, all_107_5, all_107_6, all_107_7, all_107_8 gives: % 70.81/9.81 | (59) ( ~ (all_107_0 = norm) & index(status, all_65_0) = all_107_0 & % 70.81/9.81 | $i(all_107_0)) | ( ~ (all_107_1 = all_65_0) & index(ldr, all_65_0) = % 70.81/9.81 | all_107_1 & $i(all_107_1)) | (host(all_65_5) = all_107_8 & % 70.81/9.81 | $i(all_107_8) & (( ~ (all_107_2 = all_107_5) & index(pendack, % 70.81/9.81 | all_107_8) = all_107_6 & s(all_107_6) = all_107_5 & % 70.81/9.81 | host(all_65_6) = all_107_2 & $i(all_107_2) & $i(all_107_5) & % 70.81/9.81 | $i(all_107_6)) | ( ~ (all_107_3 = all_107_6) & index(pendack, % 70.81/9.81 | all_107_8) = all_107_6 & host(all_65_7) = all_107_3 & % 70.81/9.81 | $i(all_107_3) & $i(all_107_6)) | ( ~ (all_107_4 = elec_2) & % 70.81/9.81 | index(status, all_107_8) = all_107_4 & $i(all_107_4)) | % 70.81/9.81 | (index(pendack, all_107_8) = all_107_6 & s(all_107_6) = all_107_5 % 70.81/9.81 | & $i(all_107_5) & $i(all_107_6) & ~ leq(nbr_proc, all_107_5)) | % 70.81/9.81 | (queue(all_107_8) = all_107_7 & $i(all_107_7) & ( ~ elem(all_65_3, % 70.81/9.81 | all_107_7) | ~ elem(all_65_4, all_107_7))))) % 70.81/9.81 | % 70.81/9.81 | REDUCE: (32), (47) imply: % 70.81/9.81 | (60) m_Ack(all_65_14, all_65_7) = all_65_3 % 70.81/9.81 | % 70.81/9.81 | REDUCE: (47), (58) imply: % 70.81/9.81 | (61) host(all_65_14) = all_99_3 % 70.81/9.81 | % 70.81/9.81 | REDUCE: (47), (56) imply: % 70.81/9.81 | (62) host(all_65_14) = all_96_2 % 70.81/9.81 | % 70.81/9.81 | BETA: splitting (59) gives: % 70.81/9.81 | % 70.81/9.81 | Case 1: % 70.81/9.81 | | % 70.81/9.82 | | (63) ~ (all_107_0 = norm) & index(status, all_65_0) = all_107_0 & % 70.81/9.82 | | $i(all_107_0) % 70.81/9.82 | | % 70.81/9.82 | | ALPHA: (63) implies: % 70.81/9.82 | | (64) ~ (all_107_0 = norm) % 70.81/9.82 | | (65) index(status, all_65_0) = all_107_0 % 70.81/9.82 | | % 70.81/9.82 | | GROUND_INST: instantiating (7) with norm, all_107_0, all_65_0, status, % 70.81/9.82 | | simplifying with (40), (65) gives: % 70.81/9.82 | | (66) all_107_0 = norm % 70.81/9.82 | | % 70.81/9.82 | | REDUCE: (64), (66) imply: % 70.81/9.82 | | (67) $false % 70.81/9.82 | | % 70.81/9.82 | | CLOSE: (67) is inconsistent. % 70.81/9.82 | | % 70.81/9.82 | Case 2: % 70.81/9.82 | | % 70.81/9.82 | | (68) ( ~ (all_107_1 = all_65_0) & index(ldr, all_65_0) = all_107_1 & % 70.81/9.82 | | $i(all_107_1)) | (host(all_65_5) = all_107_8 & $i(all_107_8) & (( % 70.81/9.82 | | ~ (all_107_2 = all_107_5) & index(pendack, all_107_8) = % 70.81/9.82 | | all_107_6 & s(all_107_6) = all_107_5 & host(all_65_6) = % 70.81/9.82 | | all_107_2 & $i(all_107_2) & $i(all_107_5) & $i(all_107_6)) | ( % 70.81/9.82 | | ~ (all_107_3 = all_107_6) & index(pendack, all_107_8) = % 70.81/9.82 | | all_107_6 & host(all_65_7) = all_107_3 & $i(all_107_3) & % 70.81/9.82 | | $i(all_107_6)) | ( ~ (all_107_4 = elec_2) & index(status, % 70.81/9.82 | | all_107_8) = all_107_4 & $i(all_107_4)) | (index(pendack, % 70.81/9.82 | | all_107_8) = all_107_6 & s(all_107_6) = all_107_5 & % 70.81/9.82 | | $i(all_107_5) & $i(all_107_6) & ~ leq(nbr_proc, all_107_5)) | % 70.81/9.82 | | (queue(all_107_8) = all_107_7 & $i(all_107_7) & ( ~ % 70.81/9.82 | | elem(all_65_3, all_107_7) | ~ elem(all_65_4, all_107_7))))) % 70.81/9.82 | | % 70.81/9.82 | | BETA: splitting (68) gives: % 70.81/9.82 | | % 70.81/9.82 | | Case 1: % 70.81/9.82 | | | % 70.81/9.82 | | | (69) ~ (all_107_1 = all_65_0) & index(ldr, all_65_0) = all_107_1 & % 70.81/9.82 | | | $i(all_107_1) % 70.81/9.82 | | | % 70.81/9.82 | | | ALPHA: (69) implies: % 70.81/9.82 | | | (70) ~ (all_107_1 = all_65_0) % 70.81/9.82 | | | (71) index(ldr, all_65_0) = all_107_1 % 70.81/9.82 | | | % 70.81/9.82 | | | GROUND_INST: instantiating (7) with all_65_0, all_107_1, all_65_0, ldr, % 70.81/9.82 | | | simplifying with (41), (71) gives: % 70.81/9.82 | | | (72) all_107_1 = all_65_0 % 70.81/9.82 | | | % 70.81/9.82 | | | REDUCE: (70), (72) imply: % 70.81/9.82 | | | (73) $false % 70.81/9.82 | | | % 70.81/9.82 | | | CLOSE: (73) is inconsistent. % 70.81/9.82 | | | % 70.81/9.82 | | Case 2: % 70.81/9.82 | | | % 70.81/9.82 | | | (74) host(all_65_5) = all_107_8 & $i(all_107_8) & (( ~ (all_107_2 = % 70.81/9.82 | | | all_107_5) & index(pendack, all_107_8) = all_107_6 & % 70.81/9.82 | | | s(all_107_6) = all_107_5 & host(all_65_6) = all_107_2 & % 70.81/9.82 | | | $i(all_107_2) & $i(all_107_5) & $i(all_107_6)) | ( ~ % 70.81/9.82 | | | (all_107_3 = all_107_6) & index(pendack, all_107_8) = % 70.81/9.82 | | | all_107_6 & host(all_65_7) = all_107_3 & $i(all_107_3) & % 70.81/9.82 | | | $i(all_107_6)) | ( ~ (all_107_4 = elec_2) & index(status, % 70.81/9.82 | | | all_107_8) = all_107_4 & $i(all_107_4)) | (index(pendack, % 70.81/9.82 | | | all_107_8) = all_107_6 & s(all_107_6) = all_107_5 & % 70.81/9.82 | | | $i(all_107_5) & $i(all_107_6) & ~ leq(nbr_proc, all_107_5)) | % 70.81/9.82 | | | (queue(all_107_8) = all_107_7 & $i(all_107_7) & ( ~ % 70.81/9.82 | | | elem(all_65_3, all_107_7) | ~ elem(all_65_4, all_107_7)))) % 70.81/9.82 | | | % 70.81/9.82 | | | ALPHA: (74) implies: % 70.81/9.82 | | | (75) host(all_65_5) = all_107_8 % 70.81/9.82 | | | (76) ( ~ (all_107_2 = all_107_5) & index(pendack, all_107_8) = % 70.81/9.82 | | | all_107_6 & s(all_107_6) = all_107_5 & host(all_65_6) = % 70.81/9.82 | | | all_107_2 & $i(all_107_2) & $i(all_107_5) & $i(all_107_6)) | ( ~ % 70.81/9.82 | | | (all_107_3 = all_107_6) & index(pendack, all_107_8) = all_107_6 % 70.81/9.82 | | | & host(all_65_7) = all_107_3 & $i(all_107_3) & $i(all_107_6)) | % 70.81/9.82 | | | ( ~ (all_107_4 = elec_2) & index(status, all_107_8) = all_107_4 & % 70.81/9.82 | | | $i(all_107_4)) | (index(pendack, all_107_8) = all_107_6 & % 70.81/9.82 | | | s(all_107_6) = all_107_5 & $i(all_107_5) & $i(all_107_6) & ~ % 70.81/9.82 | | | leq(nbr_proc, all_107_5)) | (queue(all_107_8) = all_107_7 & % 70.81/9.82 | | | $i(all_107_7) & ( ~ elem(all_65_3, all_107_7) | ~ % 70.81/9.82 | | | elem(all_65_4, all_107_7))) % 70.81/9.82 | | | % 70.81/9.82 | | | REDUCE: (47), (75) imply: % 70.81/9.82 | | | (77) host(all_65_14) = all_107_8 % 70.81/9.82 | | | % 70.81/9.82 | | | GROUND_INST: instantiating (5) with all_65_13, all_99_3, all_65_14, % 70.81/9.82 | | | simplifying with (27), (61) gives: % 70.81/9.82 | | | (78) all_99_3 = all_65_13 % 70.81/9.82 | | | % 70.81/9.82 | | | GROUND_INST: instantiating (5) with all_99_3, all_107_8, all_65_14, % 70.81/9.82 | | | simplifying with (61), (77) gives: % 70.81/9.82 | | | (79) all_107_8 = all_99_3 % 70.81/9.82 | | | % 70.81/9.82 | | | GROUND_INST: instantiating (5) with all_96_2, all_107_8, all_65_14, % 70.81/9.82 | | | simplifying with (62), (77) gives: % 70.81/9.82 | | | (80) all_107_8 = all_96_2 % 70.81/9.82 | | | % 70.81/9.82 | | | GROUND_INST: instantiating (6) with all_65_1, all_82_0, all_65_2, % 70.81/9.82 | | | simplifying with (33), (54) gives: % 70.81/9.82 | | | (81) all_82_0 = all_65_1 % 70.81/9.82 | | | % 70.81/9.82 | | | COMBINE_EQS: (79), (80) imply: % 70.81/9.82 | | | (82) all_99_3 = all_96_2 % 70.81/9.82 | | | % 70.81/9.82 | | | SIMP: (82) implies: % 70.81/9.82 | | | (83) all_99_3 = all_96_2 % 70.81/9.82 | | | % 70.81/9.82 | | | COMBINE_EQS: (78), (83) imply: % 70.81/9.82 | | | (84) all_96_2 = all_65_13 % 70.81/9.82 | | | % 70.81/9.82 | | | SIMP: (84) implies: % 70.81/9.82 | | | (85) all_96_2 = all_65_13 % 70.81/9.82 | | | % 70.81/9.82 | | | COMBINE_EQS: (80), (85) imply: % 70.81/9.82 | | | (86) all_107_8 = all_65_13 % 70.81/9.82 | | | % 70.81/9.82 | | | BETA: splitting (76) gives: % 70.81/9.82 | | | % 70.81/9.82 | | | Case 1: % 70.81/9.82 | | | | % 70.81/9.82 | | | | (87) ( ~ (all_107_2 = all_107_5) & index(pendack, all_107_8) = % 70.81/9.82 | | | | all_107_6 & s(all_107_6) = all_107_5 & host(all_65_6) = % 70.81/9.82 | | | | all_107_2 & $i(all_107_2) & $i(all_107_5) & $i(all_107_6)) | ( % 70.81/9.82 | | | | ~ (all_107_3 = all_107_6) & index(pendack, all_107_8) = % 70.81/9.82 | | | | all_107_6 & host(all_65_7) = all_107_3 & $i(all_107_3) & % 70.81/9.82 | | | | $i(all_107_6)) % 70.81/9.82 | | | | % 70.81/9.82 | | | | BETA: splitting (87) gives: % 70.81/9.82 | | | | % 70.81/9.82 | | | | Case 1: % 70.81/9.82 | | | | | % 70.81/9.82 | | | | | (88) ~ (all_107_2 = all_107_5) & index(pendack, all_107_8) = % 70.81/9.82 | | | | | all_107_6 & s(all_107_6) = all_107_5 & host(all_65_6) = % 70.81/9.82 | | | | | all_107_2 & $i(all_107_2) & $i(all_107_5) & $i(all_107_6) % 70.81/9.82 | | | | | % 70.81/9.82 | | | | | ALPHA: (88) implies: % 70.81/9.82 | | | | | (89) ~ (all_107_2 = all_107_5) % 70.81/9.82 | | | | | (90) host(all_65_6) = all_107_2 % 70.81/9.82 | | | | | (91) s(all_107_6) = all_107_5 % 70.81/9.82 | | | | | (92) index(pendack, all_107_8) = all_107_6 % 70.81/9.82 | | | | | % 70.81/9.82 | | | | | REDUCE: (86), (92) imply: % 70.81/9.83 | | | | | (93) index(pendack, all_65_13) = all_107_6 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (5) with all_65_1, all_107_2, all_65_6, % 70.81/9.83 | | | | | simplifying with (30), (90) gives: % 70.81/9.83 | | | | | (94) all_107_2 = all_65_1 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (7) with all_65_2, all_107_6, all_65_13, % 70.81/9.83 | | | | | pendack, simplifying with (38), (93) gives: % 70.81/9.83 | | | | | (95) all_107_6 = all_65_2 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (89), (94) imply: % 70.81/9.83 | | | | | (96) ~ (all_107_5 = all_65_1) % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | SIMP: (96) implies: % 70.81/9.83 | | | | | (97) ~ (all_107_5 = all_65_1) % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (91), (95) imply: % 70.81/9.83 | | | | | (98) s(all_65_2) = all_107_5 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (6) with all_65_1, all_107_5, all_65_2, % 70.81/9.83 | | | | | simplifying with (33), (98) gives: % 70.81/9.83 | | | | | (99) all_107_5 = all_65_1 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (97), (99) imply: % 70.81/9.83 | | | | | (100) $false % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | CLOSE: (100) is inconsistent. % 70.81/9.83 | | | | | % 70.81/9.83 | | | | Case 2: % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | (101) ~ (all_107_3 = all_107_6) & index(pendack, all_107_8) = % 70.81/9.83 | | | | | all_107_6 & host(all_65_7) = all_107_3 & $i(all_107_3) & % 70.81/9.83 | | | | | $i(all_107_6) % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | ALPHA: (101) implies: % 70.81/9.83 | | | | | (102) ~ (all_107_3 = all_107_6) % 70.81/9.83 | | | | | (103) host(all_65_7) = all_107_3 % 70.81/9.83 | | | | | (104) index(pendack, all_107_8) = all_107_6 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (86), (104) imply: % 70.81/9.83 | | | | | (105) index(pendack, all_65_13) = all_107_6 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (5) with all_65_2, all_107_3, all_65_7, % 70.81/9.83 | | | | | simplifying with (29), (103) gives: % 70.81/9.83 | | | | | (106) all_107_3 = all_65_2 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (7) with all_65_2, all_107_6, all_65_13, % 70.81/9.83 | | | | | pendack, simplifying with (38), (105) gives: % 70.81/9.83 | | | | | (107) all_107_6 = all_65_2 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (102), (106), (107) imply: % 70.81/9.83 | | | | | (108) $false % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | CLOSE: (108) is inconsistent. % 70.81/9.83 | | | | | % 70.81/9.83 | | | | End of split % 70.81/9.83 | | | | % 70.81/9.83 | | | Case 2: % 70.81/9.83 | | | | % 70.81/9.83 | | | | (109) ( ~ (all_107_4 = elec_2) & index(status, all_107_8) = all_107_4 % 70.81/9.83 | | | | & $i(all_107_4)) | (index(pendack, all_107_8) = all_107_6 & % 70.81/9.83 | | | | s(all_107_6) = all_107_5 & $i(all_107_5) & $i(all_107_6) & ~ % 70.81/9.83 | | | | leq(nbr_proc, all_107_5)) | (queue(all_107_8) = all_107_7 & % 70.81/9.83 | | | | $i(all_107_7) & ( ~ elem(all_65_3, all_107_7) | ~ % 70.81/9.83 | | | | elem(all_65_4, all_107_7))) % 70.81/9.83 | | | | % 70.81/9.83 | | | | BETA: splitting (109) gives: % 70.81/9.83 | | | | % 70.81/9.83 | | | | Case 1: % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | (110) ~ (all_107_4 = elec_2) & index(status, all_107_8) = % 70.81/9.83 | | | | | all_107_4 & $i(all_107_4) % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | ALPHA: (110) implies: % 70.81/9.83 | | | | | (111) ~ (all_107_4 = elec_2) % 70.81/9.83 | | | | | (112) index(status, all_107_8) = all_107_4 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (86), (112) imply: % 70.81/9.83 | | | | | (113) index(status, all_65_13) = all_107_4 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | GROUND_INST: instantiating (7) with elec_2, all_107_4, all_65_13, % 70.81/9.83 | | | | | status, simplifying with (39), (113) gives: % 70.81/9.83 | | | | | (114) all_107_4 = elec_2 % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | REDUCE: (111), (114) imply: % 70.81/9.83 | | | | | (115) $false % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | CLOSE: (115) is inconsistent. % 70.81/9.83 | | | | | % 70.81/9.83 | | | | Case 2: % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | (116) (index(pendack, all_107_8) = all_107_6 & s(all_107_6) = % 70.81/9.83 | | | | | all_107_5 & $i(all_107_5) & $i(all_107_6) & ~ % 70.81/9.83 | | | | | leq(nbr_proc, all_107_5)) | (queue(all_107_8) = all_107_7 & % 70.81/9.83 | | | | | $i(all_107_7) & ( ~ elem(all_65_3, all_107_7) | ~ % 70.81/9.83 | | | | | elem(all_65_4, all_107_7))) % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | BETA: splitting (116) gives: % 70.81/9.83 | | | | | % 70.81/9.83 | | | | | Case 1: % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | (117) index(pendack, all_107_8) = all_107_6 & s(all_107_6) = % 70.81/9.83 | | | | | | all_107_5 & $i(all_107_5) & $i(all_107_6) & ~ % 70.81/9.83 | | | | | | leq(nbr_proc, all_107_5) % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | ALPHA: (117) implies: % 70.81/9.83 | | | | | | (118) ~ leq(nbr_proc, all_107_5) % 70.81/9.83 | | | | | | (119) s(all_107_6) = all_107_5 % 70.81/9.83 | | | | | | (120) index(pendack, all_107_8) = all_107_6 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | REDUCE: (86), (120) imply: % 70.81/9.83 | | | | | | (121) index(pendack, all_65_13) = all_107_6 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | GROUND_INST: instantiating (7) with all_65_2, all_107_6, all_65_13, % 70.81/9.83 | | | | | | pendack, simplifying with (38), (121) gives: % 70.81/9.83 | | | | | | (122) all_107_6 = all_65_2 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | REDUCE: (119), (122) imply: % 70.81/9.83 | | | | | | (123) s(all_65_2) = all_107_5 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | GROUND_INST: instantiating (6) with all_65_1, all_107_5, all_65_2, % 70.81/9.83 | | | | | | simplifying with (33), (123) gives: % 70.81/9.83 | | | | | | (124) all_107_5 = all_65_1 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | REDUCE: (118), (124) imply: % 70.81/9.83 | | | | | | (125) ~ leq(nbr_proc, all_65_1) % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | PRED_UNIFY: (14), (125) imply: % 70.81/9.83 | | | | | | (126) $false % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | CLOSE: (126) is inconsistent. % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | Case 2: % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | (127) queue(all_107_8) = all_107_7 & $i(all_107_7) & ( ~ % 70.81/9.83 | | | | | | elem(all_65_3, all_107_7) | ~ elem(all_65_4, all_107_7)) % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | ALPHA: (127) implies: % 70.81/9.83 | | | | | | (128) queue(all_107_8) = all_107_7 % 70.81/9.83 | | | | | | (129) ~ elem(all_65_3, all_107_7) | ~ elem(all_65_4, all_107_7) % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | REDUCE: (86), (128) imply: % 70.81/9.83 | | | | | | (130) queue(all_65_13) = all_107_7 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | GROUND_INST: instantiating (4) with all_65_12, all_107_7, all_65_13, % 70.81/9.83 | | | | | | simplifying with (26), (130) gives: % 70.81/9.83 | | | | | | (131) all_107_7 = all_65_12 % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | BETA: splitting (52) gives: % 70.81/9.83 | | | | | | % 70.81/9.83 | | | | | | Case 1: % 70.81/9.83 | | | | | | | % 70.81/9.83 | | | | | | | (132) elem(all_65_4, all_65_16) % 70.81/9.83 | | | | | | | % 70.81/9.83 | | | | | | | BETA: splitting (51) gives: % 70.81/9.83 | | | | | | | % 70.81/9.83 | | | | | | | Case 1: % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | | (133) elem(all_65_3, all_65_16) % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | | GROUND_INST: instantiating (1) with all_65_4, all_65_11, % 70.81/9.83 | | | | | | | | all_65_16, all_65_12, simplifying with (15), (18), % 70.81/9.83 | | | | | | | | (24), (36), (132) gives: % 70.81/9.83 | | | | | | | | (134) elem(all_65_4, all_65_12) % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | | GROUND_INST: instantiating (1) with all_65_3, all_65_11, % 70.81/9.83 | | | | | | | | all_65_16, all_65_12, simplifying with (15), (18), % 70.81/9.83 | | | | | | | | (25), (36), (133) gives: % 70.81/9.83 | | | | | | | | (135) elem(all_65_3, all_65_12) % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | | BETA: splitting (129) gives: % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | | Case 1: % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | (136) ~ elem(all_65_3, all_107_7) % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | REDUCE: (131), (136) imply: % 70.81/9.83 | | | | | | | | | (137) ~ elem(all_65_3, all_65_12) % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | PRED_UNIFY: (135), (137) imply: % 70.81/9.83 | | | | | | | | | (138) $false % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | CLOSE: (138) is inconsistent. % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | Case 2: % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | (139) ~ elem(all_65_4, all_107_7) % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | REDUCE: (131), (139) imply: % 70.81/9.83 | | | | | | | | | (140) ~ elem(all_65_4, all_65_12) % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | PRED_UNIFY: (134), (140) imply: % 70.81/9.83 | | | | | | | | | (141) $false % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | | CLOSE: (141) is inconsistent. % 70.81/9.83 | | | | | | | | | % 70.81/9.83 | | | | | | | | End of split % 70.81/9.83 | | | | | | | | % 70.81/9.83 | | | | | | | Case 2: % 70.81/9.83 | | | | | | | | % 70.81/9.84 | | | | | | | | (142) all_65_3 = all_65_10 % 70.81/9.84 | | | | | | | | % 70.81/9.84 | | | | | | | | REDUCE: (60), (142) imply: % 70.81/9.84 | | | | | | | | (143) m_Ack(all_65_14, all_65_7) = all_65_10 % 70.81/9.84 | | | | | | | | % 70.81/9.84 | | | | | | | | GROUND_INST: instantiating (axiom_13) with all_65_14, all_65_7, % 70.81/9.84 | | | | | | | | all_65_15, all_65_10, simplifying with (16), (17), % 70.81/9.84 | | | | | | | | (21), (35), (143) gives: % 70.81/9.84 | | | | | | | | (144) $false % 70.81/9.84 | | | | | | | | % 70.81/9.84 | | | | | | | | CLOSE: (144) is inconsistent. % 70.81/9.84 | | | | | | | | % 70.81/9.84 | | | | | | | End of split % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | Case 2: % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | | (145) all_65_4 = all_65_10 % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | | REDUCE: (34), (145) imply: % 70.81/9.84 | | | | | | | (146) m_Down(all_65_6) = all_65_10 % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | | GROUND_INST: instantiating (axiom_19) with all_65_6, all_65_15, % 70.81/9.84 | | | | | | | all_65_10, simplifying with (16), (22), (35), (146) % 70.81/9.84 | | | | | | | gives: % 70.81/9.84 | | | | | | | (147) $false % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | | CLOSE: (147) is inconsistent. % 70.81/9.84 | | | | | | | % 70.81/9.84 | | | | | | End of split % 70.81/9.84 | | | | | | % 70.81/9.84 | | | | | End of split % 70.81/9.84 | | | | | % 70.81/9.84 | | | | End of split % 70.81/9.84 | | | | % 70.81/9.84 | | | End of split % 70.81/9.84 | | | % 70.81/9.84 | | End of split % 70.81/9.84 | | % 70.81/9.84 | End of split % 70.81/9.84 | % 70.81/9.84 End of proof % 70.81/9.84 % SZS output end Proof for theBenchmark % 70.81/9.84 % 70.81/9.84 9309ms %------------------------------------------------------------------------------