%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SWV472+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n009.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 : 600s % DateTime : Wed Jul 20 17:51:41 EDT 2022 % Result : Theorem 245.10s 181.58s % Output : Proof 251.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV472+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n009.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 14 15:41:08 EDT 2022 % 0.13/0.34 % CPUTime : % 0.54/0.61 ____ _ % 0.54/0.61 ___ / __ \_____(_)___ ________ __________ % 0.54/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.54/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.54/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.54/0.61 % 0.54/0.61 A Theorem Prover for First-Order Logic % 0.54/0.61 (ePrincess v.1.0) % 0.54/0.61 % 0.54/0.61 (c) Philipp Rümmer, 2009-2015 % 0.54/0.61 (c) Peter Backeman, 2014-2015 % 0.54/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.54/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.54/0.61 Bug reports to peter@backeman.se % 0.54/0.61 % 0.54/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.54/0.61 % 0.54/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.75/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.02/1.05 Prover 0: Preprocessing ... % 3.68/1.49 Prover 0: Warning: ignoring some quantifiers % 3.68/1.52 Prover 0: Constructing countermodel ... % 18.48/5.95 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.84/6.06 Prover 1: Preprocessing ... % 19.99/6.26 Prover 1: Constructing countermodel ... % 21.87/6.74 Prover 1: gave up % 21.87/6.74 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 22.35/6.78 Prover 2: Preprocessing ... % 23.09/6.97 Prover 2: Warning: ignoring some quantifiers % 23.09/6.98 Prover 2: Constructing countermodel ... % 29.19/8.45 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 29.47/8.52 Prover 3: Preprocessing ... % 29.98/8.62 Prover 3: Warning: ignoring some quantifiers % 29.98/8.62 Prover 3: Constructing countermodel ... % 33.65/9.57 Prover 3: gave up % 33.65/9.57 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 34.04/9.60 Prover 4: Preprocessing ... % 34.64/9.76 Prover 4: Warning: ignoring some quantifiers % 34.64/9.76 Prover 4: Constructing countermodel ... % 39.89/11.86 Prover 0: stopped % 40.26/12.06 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 40.47/12.11 Prover 5: Preprocessing ... % 40.82/12.23 Prover 5: Constructing countermodel ... % 56.41/25.15 Prover 5: stopped % 56.64/25.35 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 56.64/25.40 Prover 6: Preprocessing ... % 57.20/25.54 Prover 6: Warning: ignoring some quantifiers % 57.20/25.54 Prover 6: Constructing countermodel ... % 135.68/95.37 Prover 2: stopped % 135.94/95.57 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 136.07/95.63 Prover 7: Preprocessing ... % 136.12/95.72 Prover 7: Proving ... % 187.71/136.26 Prover 4: stopped % 187.93/136.46 Prover 8: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 188.14/136.54 Prover 8: Preprocessing ... % 188.36/136.62 Prover 8: Constructing countermodel ... % 189.65/136.88 Prover 8: gave up % 189.65/136.88 Prover 9: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=completeFrugal % 189.65/136.92 Prover 9: Preprocessing ... % 190.29/136.98 Prover 9: Proving ... % 208.09/151.50 Prover 9: stopped % 208.29/151.70 Prover 10: Options: -triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 208.38/151.75 Prover 10: Preprocessing ... % 208.38/151.81 Prover 10: Warning: ignoring some quantifiers % 208.38/151.82 Prover 10: Constructing countermodel ... % 243.53/180.91 Prover 6: stopped % 243.72/181.11 Prover 11: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 243.85/181.16 Prover 11: Preprocessing ... % 244.03/181.22 Prover 11: Warning: ignoring some quantifiers % 244.03/181.22 Prover 11: Constructing countermodel ... % 245.10/181.57 Prover 11: proved (466ms) % 245.10/181.58 Prover 7: stopped % 245.10/181.58 Prover 10: stopped % 245.10/181.58 % 245.10/181.58 No countermodel exists, formula is valid % 245.10/181.58 % SZS status Theorem for theBenchmark % 245.10/181.58 % 245.10/181.58 Generating proof ... Warning: ignoring some quantifiers % 251.25/184.25 found it (size 86) % 251.25/184.25 % 251.25/184.25 % SZS output start Proof for theBenchmark % 251.25/184.25 Assumed formulas after preprocessing and simplification: % 251.25/184.25 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ( ~ (v5 = nbr_proc) & ~ (norm = wait) & ~ (norm = elec_1) & ~ (norm = elec_2) & ~ (wait = elec_1) & ~ (wait = elec_2) & ~ (elec_1 = elec_2) & index(pendack, v5) = v8 & index(down, nbr_proc) = v15 & index(elid, v5) = v2 & index(status, v5) = elec_2 & index(status, nbr_proc) = elec_1 & snoc(v1, v9) = v10 & cons(v7, v1) = v6 & m_Down(v13) = v17 & m_Down(v12) = v19 & m_Halt(v3) = v9 & s(v8) = v5 & s(zero) = v0 & m_Ack(v2, v4) = v7 & host(v14) = nbr_proc & host(v13) = v16 & host(v12) = nbr_proc & host(v11) = v5 & host(v4) = v8 & host(v3) = v5 & queue(v5) = v6 & queue(nbr_proc) = v18 & ordered(q_nil) & leq(v0, nbr_proc) & setIn(v11, alive) & setIn(v3, alive) & elem(v19, v10) & elem(v17, v18) & ~ leq(nbr_proc, v8) & ~ setIn(nil, alive) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (m_Down(v23) = v26) | ~ (m_Down(v21) = v27) | ~ (host(v22) = v24) | ~ (host(v20) = v25) | ~ setIn(v22, alive) | ~ setIn(v20, alive) | ? [v28] : (( ~ (v28 = v25) & host(v21) = v28) | ( ~ (v28 = v24) & host(v23) = v28) | (queue(v25) = v28 & ~ elem(v26, v28)) | (queue(v24) = v28 & ~ elem(v27, v28)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v25 = v24 | ~ (m_Down(v23) = v26) | ~ (host(v22) = v24) | ~ (host(v21) = v25) | ~ (host(v20) = v25) | ~ setIn(v22, alive) | ~ setIn(v20, alive) | ? [v27] : (( ~ (v27 = v24) & host(v23) = v27) | (index(down, v24) = v27 & ~ setIn(v25, v27)) | (queue(v25) = v27 & ~ elem(v26, v27)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ! [v26] : ( ~ (m_Down(v22) = v24) | ~ (m_Down(v21) = v25) | ~ (host(v23) = nbr_proc) | ~ (host(v20) = v26) | ~ setIn(v20, alive) | ? [v27] : ? [v28] : ? [v29] : ((v27 = v18 & ~ elem(v24, v18)) | (v27 = v15 & ~ (v29 = v28) & host(v22) = v28 & leq(v0, v29) & ~ leq(nbr_proc, v29) & ~ setIn(v29, v15)) | ( ~ (v27 = nbr_proc) & host(v21) = v27) | (queue(v26) = v27 & ~ elem(v25, v27)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : (v24 = v23 | ~ (m_Down(v20) = v25) | ~ (host(v22) = v23) | ~ (host(v21) = v24) | ~ setIn(v22, alive) | ? [v26] : ? [v27] : (( ~ (v27 = v24) & index(elid, v23) = v26 & host(v26) = v27) | ( ~ (v26 = v23) & host(v20) = v26) | ( ~ (v26 = wait) & index(status, v23) = v26) | (queue(v24) = v26 & ~ elem(v25, v26)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : (v24 = v23 | ~ (m_Down(v20) = v25) | ~ (host(v22) = v23) | ~ (host(v21) = v24) | ~ setIn(v22, alive) | ? [v26] : (( ~ (v26 = v24) & index(ldr, v23) = v26) | ( ~ (v26 = v23) & host(v20) = v26) | ( ~ (v26 = norm) & index(status, v23) = v26) | (queue(v24) = v26 & ~ elem(v25, v26)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ( ~ (cons(v23, v20) = v24) | ~ (m_Down(v22) = v25) | ~ (m_Halt(v21) = v23) | ~ ordered(v24) | ~ elem(v25, v20) | leq(v21, v22) | ? [v26] : ? [v27] : ( ~ (v27 = v26) & host(v22) = v27 & host(v21) = v26)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v23 = v22 | ~ (m_Ack(v21, v23) = v24) | ~ (m_Ack(v20, v22) = v24)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : (v21 = v20 | ~ (m_Ack(v21, v23) = v24) | ~ (m_Ack(v20, v22) = v24)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (snoc(v22, v21) = v23) | ~ (cons(v20, v23) = v24) | ? [v25] : (snoc(v25, v21) = v24 & cons(v20, v22) = v25)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ( ~ (snoc(v20, v23) = v24) | ~ (m_Ack(v21, v22) = v23) | ~ ordered(v20) | ordered(v24)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = v20 | v20 = q_nil | ~ (init(v20) = v21) | ~ (snoc(v21, v22) = v23) | ~ (last(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = v20 | v20 = q_nil | ~ (tail(v20) = v22) | ~ (cons(v21, v22) = v23) | ~ (head(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (index(v23, v22) = v21) | ~ (index(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (snoc(v23, v22) = v21) | ~ (snoc(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (snoc(v22, v21) = v23) | ~ elem(v20, v23) | elem(v20, v22)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (cons(v23, v22) = v21) | ~ (cons(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (cons(v21, v22) = v23) | ~ elem(v20, v23) | elem(v20, v22)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v20 | ~ (m_Ack(v23, v22) = v21) | ~ (m_Ack(v23, v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (snoc(v22, v21) = v23) | ~ elem(v20, v22) | elem(v20, v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (snoc(v20, v22) = v23) | ~ (m_Ldr(v21) = v22) | ~ ordered(v20) | ordered(v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (cons(v21, v22) = v23) | ~ elem(v20, v22) | elem(v20, v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_NormQ(v22) = v23) | ~ (m_Ack(v20, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_Ldr(v22) = v23) | ~ (m_Ack(v20, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_Ldr(v21) = v22) | ~ (host(v20) = v23) | ? [v24] : ((host(v21) = v24 & ~ leq(v23, v24)) | (queue(v23) = v24 & ~ elem(v22, v24)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_NotNorm(v22) = v23) | ~ (m_Ack(v20, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_Down(v22) = v23) | ~ (m_Ack(v20, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_Down(v21) = v22) | ~ (host(v20) = v23) | ? [v24] : (( ~ (v24 = v23) & host(v21) = v24) | (queue(v23) = v24 & ~ elem(v22, v24)))) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (m_Halt(v22) = v23) | ~ (m_Ack(v20, v21) = v23)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (s(v21) = v23) | ~ (s(v20) = v22) | ~ leq(v22, v23) | leq(v20, v21)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (s(v21) = v23) | ~ (s(v20) = v22) | ~ leq(v20, v21) | leq(v22, v23)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (m_NormQ(v20) = v22) | ~ (m_NormQ(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (m_Ldr(v20) = v22) | ~ (m_Ldr(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (m_NotNorm(v20) = v22) | ~ (m_NotNorm(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (m_Down(v20) = v22) | ~ (m_Down(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (m_Halt(v20) = v22) | ~ (m_Halt(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v21 | ~ (host(v20) = v22) | ~ (host(v20) = v21)) & ! [v20] : ! [v21] : ! [v22] : (v22 = v20 | ~ (s(v21) = v22) | ~ leq(v20, v22) | leq(v20, v21)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (pidMsg(v22) = v21) | ~ (pidMsg(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (init(v22) = v21) | ~ (init(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (last(v22) = v21) | ~ (last(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (tail(v22) = v21) | ~ (tail(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (head(v22) = v21) | ~ (head(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_NormQ(v22) = v21) | ~ (m_NormQ(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_NormQ(v21) = v22) | ~ (m_NormQ(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Ldr(v22) = v21) | ~ (m_Ldr(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Ldr(v21) = v22) | ~ (m_Ldr(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_NotNorm(v22) = v21) | ~ (m_NotNorm(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_NotNorm(v21) = v22) | ~ (m_NotNorm(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Down(v22) = v21) | ~ (m_Down(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Down(v21) = v22) | ~ (m_Down(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Halt(v22) = v21) | ~ (m_Halt(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (m_Halt(v21) = v22) | ~ (m_Halt(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (s(v22) = v21) | ~ (s(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (host(v22) = v21) | ~ (host(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (host(v21) = v22) | ~ (host(v20) = v22) | ~ setIn(v21, alive) | ~ setIn(v20, alive)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (queue(v22) = v21) | ~ (queue(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | ~ ordered(v22) | ordered(v21)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | ~ ordered(v22) | ? [v23] : ? [v24] : (pidMsg(v20) = v23 & host(v23) = v24 & ! [v25] : ! [v26] : ( ~ (pidMsg(v25) = v26) | ~ pidElem(v25) | ~ pidElem(v20) | ~ elem(v25, v21) | leq(v26, v23) | ? [v27] : ( ~ (v27 = v24) & host(v26) = v27)))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | ~ ordered(v21) | ordered(v22) | ? [v23] : ? [v24] : ? [v25] : ? [v26] : (pidMsg(v25) = v26 & pidMsg(v20) = v23 & host(v26) = v24 & host(v23) = v24 & pidElem(v25) & pidElem(v20) & elem(v25, v21) & ~ leq(v26, v23))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | init(v22) = v21) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | last(v22) = v20) & ! [v20] : ! [v21] : ! [v22] : ( ~ (snoc(v21, v20) = v22) | elem(v20, v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | ~ ordered(v22) | ordered(v21)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | ~ ordered(v22) | ? [v23] : ? [v24] : (pidMsg(v20) = v23 & host(v23) = v24 & ! [v25] : ! [v26] : ( ~ (pidMsg(v25) = v26) | ~ pidElem(v25) | ~ pidElem(v20) | ~ elem(v25, v21) | leq(v23, v26) | ? [v27] : ( ~ (v27 = v24) & host(v26) = v27)))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | ~ ordered(v21) | ordered(v22) | ? [v23] : ? [v24] : ? [v25] : ? [v26] : (pidMsg(v25) = v26 & pidMsg(v20) = v23 & host(v26) = v24 & host(v23) = v24 & pidElem(v25) & pidElem(v20) & elem(v25, v21) & ~ leq(v23, v26))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | tail(v22) = v21) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | head(v22) = v20) & ! [v20] : ! [v21] : ! [v22] : ( ~ (cons(v20, v21) = v22) | elem(v20, v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NormQ(v21) = v22) | ~ (m_Ldr(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NormQ(v21) = v22) | ~ (m_Down(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NormQ(v20) = v22) | ~ (m_NotNorm(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NormQ(v20) = v22) | ~ (m_Halt(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Ldr(v21) = v22) | ~ (m_Down(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Ldr(v20) = v22) | ~ (m_NotNorm(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Ldr(v20) = v22) | ~ (m_Halt(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NotNorm(v21) = v22) | ~ (m_Down(v20) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NotNorm(v20) = v22) | ~ (m_Halt(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_NotNorm(v20) = v22) | ~ (host(v21) = nbr_proc) | ~ elem(v22, v18)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Down(v20) = v22) | ~ (m_Halt(v21) = v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (s(v21) = v22) | ~ leq(v20, v21) | leq(v20, v22)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Ack(v20, v21) = v22) | setIn(v21, pids) | ? [v23] : ? [v24] : (host(v20) = v23 & queue(v23) = v24 & ~ elem(v22, v24))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (m_Ack(v20, v21) = v22) | setIn(v20, pids) | ? [v23] : ? [v24] : (host(v20) = v23 & queue(v23) = v24 & ~ elem(v22, v24))) & ! [v20] : ! [v21] : ! [v22] : ( ~ (host(v21) = v22) | ~ (host(v20) = v22) | ? [v23] : ( ~ (v23 = v22) & s(v22) = v23)) & ! [v20] : ! [v21] : ! [v22] : ( ~ leq(v21, v22) | ~ leq(v20, v21) | leq(v20, v22)) & ! [v20] : ! [v21] : (v21 = v20 | ~ leq(v21, v20) | ~ leq(v20, v21)) & ! [v20] : ! [v21] : ~ (snoc(v21, v20) = q_nil) & ! [v20] : ! [v21] : ( ~ (snoc(q_nil, v20) = v21) | ordered(v21)) & ! [v20] : ! [v21] : ~ (cons(v20, v21) = q_nil) & ! [v20] : ! [v21] : ( ~ (cons(v20, q_nil) = v21) | snoc(q_nil, v20) = v21) & ! [v20] : ! [v21] : ( ~ (cons(v20, q_nil) = v21) | ordered(v21)) & ! [v20] : ! [v21] : ( ~ (m_Down(v21) = v20) | pidElem(v20)) & ! [v20] : ! [v21] : ( ~ (m_Down(v20) = v21) | pidMsg(v21) = v20) & ! [v20] : ! [v21] : ( ~ (m_Halt(v21) = v20) | pidElem(v20)) & ! [v20] : ! [v21] : ( ~ (m_Halt(v20) = v21) | pidMsg(v21) = v20) & ! [v20] : ! [v21] : ( ~ (s(v21) = v20) | leq(v20, v20)) & ! [v20] : ! [v21] : ( ~ (s(v20) = v21) | ~ leq(v21, v20)) & ! [v20] : ! [v21] : ( ~ (host(v20) = v21) | ~ setIn(v20, alive) | ? [v22] : ((v22 = v20 & index(elid, v21) = v20) | ( ~ (v22 = elec_1) & ~ (v22 = elec_2) & index(status, v21) = v22))) & ! [v20] : ! [v21] : ( ~ (host(v20) = v21) | leq(v21, nbr_proc)) & ! [v20] : ! [v21] : ( ~ (host(v20) = v21) | leq(v0, v21)) & ! [v20] : (v20 = v16 | ~ leq(v0, v20) | leq(nbr_proc, v20) | setIn(v20, v15)) & ! [v20] : ( ~ pidElem(v20) | ? [v21] : ? [v22] : ((v22 = v20 & m_Down(v21) = v20) | (v22 = v20 & m_Halt(v21) = v20))) & ! [v20] : ~ setIn(v20, setEmpty) & ! [v20] : ~ elem(v20, q_nil) & ? [v20] : ? [v21] : ? [v22] : index(v21, v20) = v22 & ? [v20] : ? [v21] : ? [v22] : snoc(v21, v20) = v22 & ? [v20] : ? [v21] : ? [v22] : cons(v21, v20) = v22 & ? [v20] : ? [v21] : ? [v22] : m_Ack(v21, v20) = v22 & ? [v20] : ? [v21] : pidMsg(v20) = v21 & ? [v20] : ? [v21] : init(v20) = v21 & ? [v20] : ? [v21] : last(v20) = v21 & ? [v20] : ? [v21] : tail(v20) = v21 & ? [v20] : ? [v21] : head(v20) = v21 & ? [v20] : ? [v21] : m_NormQ(v20) = v21 & ? [v20] : ? [v21] : m_Ldr(v20) = v21 & ? [v20] : ? [v21] : m_NotNorm(v20) = v21 & ? [v20] : ? [v21] : m_Down(v20) = v21 & ? [v20] : ? [v21] : m_Halt(v20) = v21 & ? [v20] : ? [v21] : s(v20) = v21 & ? [v20] : ? [v21] : host(v20) = v21 & ? [v20] : ? [v21] : queue(v20) = v21 & ? [v20] : ? [v21] : (leq(v21, v20) | leq(v20, v21)) & ? [v20] : leq(v20, v20)) % 251.65/184.31 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19 yields: % 251.65/184.31 | (1) ~ (all_0_14_14 = nbr_proc) & ~ (norm = wait) & ~ (norm = elec_1) & ~ (norm = elec_2) & ~ (wait = elec_1) & ~ (wait = elec_2) & ~ (elec_1 = elec_2) & index(pendack, all_0_14_14) = all_0_11_11 & index(down, nbr_proc) = all_0_4_4 & index(elid, all_0_14_14) = all_0_17_17 & index(status, all_0_14_14) = elec_2 & index(status, nbr_proc) = elec_1 & snoc(all_0_18_18, all_0_10_10) = all_0_9_9 & cons(all_0_12_12, all_0_18_18) = all_0_13_13 & m_Down(all_0_6_6) = all_0_2_2 & m_Down(all_0_7_7) = all_0_0_0 & m_Halt(all_0_16_16) = all_0_10_10 & s(all_0_11_11) = all_0_14_14 & s(zero) = all_0_19_19 & m_Ack(all_0_17_17, all_0_15_15) = all_0_12_12 & host(all_0_5_5) = nbr_proc & host(all_0_6_6) = all_0_3_3 & host(all_0_7_7) = nbr_proc & host(all_0_8_8) = all_0_14_14 & host(all_0_15_15) = all_0_11_11 & host(all_0_16_16) = all_0_14_14 & queue(all_0_14_14) = all_0_13_13 & queue(nbr_proc) = all_0_1_1 & ordered(q_nil) & leq(all_0_19_19, nbr_proc) & setIn(all_0_8_8, alive) & setIn(all_0_16_16, alive) & elem(all_0_0_0, all_0_9_9) & elem(all_0_2_2, all_0_1_1) & ~ leq(nbr_proc, all_0_11_11) & ~ setIn(nil, alive) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (m_Down(v3) = v6) | ~ (m_Down(v1) = v7) | ~ (host(v2) = v4) | ~ (host(v0) = v5) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v8] : (( ~ (v8 = v5) & host(v1) = v8) | ( ~ (v8 = v4) & host(v3) = v8) | (queue(v5) = v8 & ~ elem(v6, v8)) | (queue(v4) = v8 & ~ elem(v7, v8)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (m_Down(v3) = v6) | ~ (host(v2) = v4) | ~ (host(v1) = v5) | ~ (host(v0) = v5) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v7] : (( ~ (v7 = v4) & host(v3) = v7) | (index(down, v4) = v7 & ~ setIn(v5, v7)) | (queue(v5) = v7 & ~ elem(v6, v7)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (m_Down(v2) = v4) | ~ (m_Down(v1) = v5) | ~ (host(v3) = nbr_proc) | ~ (host(v0) = v6) | ~ setIn(v0, alive) | ? [v7] : ? [v8] : ? [v9] : ((v7 = all_0_1_1 & ~ elem(v4, all_0_1_1)) | (v7 = all_0_4_4 & ~ (v9 = v8) & host(v2) = v8 & leq(all_0_19_19, v9) & ~ leq(nbr_proc, v9) & ~ setIn(v9, all_0_4_4)) | ( ~ (v7 = nbr_proc) & host(v1) = v7) | (queue(v6) = v7 & ~ elem(v5, v7)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (m_Down(v0) = v5) | ~ (host(v2) = v3) | ~ (host(v1) = v4) | ~ setIn(v2, alive) | ? [v6] : ? [v7] : (( ~ (v7 = v4) & index(elid, v3) = v6 & host(v6) = v7) | ( ~ (v6 = v3) & host(v0) = v6) | ( ~ (v6 = wait) & index(status, v3) = v6) | (queue(v4) = v6 & ~ elem(v5, v6)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (m_Down(v0) = v5) | ~ (host(v2) = v3) | ~ (host(v1) = v4) | ~ setIn(v2, alive) | ? [v6] : (( ~ (v6 = v4) & index(ldr, v3) = v6) | ( ~ (v6 = v3) & host(v0) = v6) | ( ~ (v6 = norm) & index(status, v3) = v6) | (queue(v4) = v6 & ~ elem(v5, v6)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cons(v3, v0) = v4) | ~ (m_Down(v2) = v5) | ~ (m_Halt(v1) = v3) | ~ ordered(v4) | ~ elem(v5, v0) | leq(v1, v2) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & host(v2) = v7 & host(v1) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (m_Ack(v1, v3) = v4) | ~ (m_Ack(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (m_Ack(v1, v3) = v4) | ~ (m_Ack(v0, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (snoc(v2, v1) = v3) | ~ (cons(v0, v3) = v4) | ? [v5] : (snoc(v5, v1) = v4 & cons(v0, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (snoc(v0, v3) = v4) | ~ (m_Ack(v1, v2) = v3) | ~ ordered(v0) | ordered(v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | v0 = q_nil | ~ (init(v0) = v1) | ~ (snoc(v1, v2) = v3) | ~ (last(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | v0 = q_nil | ~ (tail(v0) = v2) | ~ (cons(v1, v2) = v3) | ~ (head(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (snoc(v3, v2) = v1) | ~ (snoc(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (snoc(v2, v1) = v3) | ~ elem(v0, v3) | elem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cons(v1, v2) = v3) | ~ elem(v0, v3) | elem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m_Ack(v3, v2) = v1) | ~ (m_Ack(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (snoc(v2, v1) = v3) | ~ elem(v0, v2) | elem(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (snoc(v0, v2) = v3) | ~ (m_Ldr(v1) = v2) | ~ ordered(v0) | ordered(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (cons(v1, v2) = v3) | ~ elem(v0, v2) | elem(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_NormQ(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Ldr(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Ldr(v1) = v2) | ~ (host(v0) = v3) | ? [v4] : ((host(v1) = v4 & ~ leq(v3, v4)) | (queue(v3) = v4 & ~ elem(v2, v4)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_NotNorm(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Down(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Down(v1) = v2) | ~ (host(v0) = v3) | ? [v4] : (( ~ (v4 = v3) & host(v1) = v4) | (queue(v3) = v4 & ~ elem(v2, v4)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Halt(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v1) = v3) | ~ (s(v0) = v2) | ~ leq(v2, v3) | leq(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v1) = v3) | ~ (s(v0) = v2) | ~ leq(v0, v1) | leq(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_NormQ(v0) = v2) | ~ (m_NormQ(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Ldr(v0) = v2) | ~ (m_Ldr(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_NotNorm(v0) = v2) | ~ (m_NotNorm(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Down(v0) = v2) | ~ (m_Down(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Halt(v0) = v2) | ~ (m_Halt(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (host(v0) = v2) | ~ (host(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (s(v1) = v2) | ~ leq(v0, v2) | leq(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (pidMsg(v2) = v1) | ~ (pidMsg(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (init(v2) = v1) | ~ (init(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (last(v2) = v1) | ~ (last(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (tail(v2) = v1) | ~ (tail(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (head(v2) = v1) | ~ (head(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NormQ(v2) = v1) | ~ (m_NormQ(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NormQ(v1) = v2) | ~ (m_NormQ(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Ldr(v2) = v1) | ~ (m_Ldr(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Ldr(v1) = v2) | ~ (m_Ldr(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NotNorm(v2) = v1) | ~ (m_NotNorm(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NotNorm(v1) = v2) | ~ (m_NotNorm(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Down(v2) = v1) | ~ (m_Down(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Down(v1) = v2) | ~ (m_Down(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Halt(v2) = v1) | ~ (m_Halt(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Halt(v1) = v2) | ~ (m_Halt(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (host(v2) = v1) | ~ (host(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (host(v1) = v2) | ~ (host(v0) = v2) | ~ setIn(v1, alive) | ~ setIn(v0, alive)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (queue(v2) = v1) | ~ (queue(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v2) | ordered(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v2) | ? [v3] : ? [v4] : (pidMsg(v0) = v3 & host(v3) = v4 & ! [v5] : ! [v6] : ( ~ (pidMsg(v5) = v6) | ~ pidElem(v5) | ~ pidElem(v0) | ~ elem(v5, v1) | leq(v6, v3) | ? [v7] : ( ~ (v7 = v4) & host(v6) = v7)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v1) | ordered(v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (pidMsg(v5) = v6 & pidMsg(v0) = v3 & host(v6) = v4 & host(v3) = v4 & pidElem(v5) & pidElem(v0) & elem(v5, v1) & ~ leq(v6, v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | init(v2) = v1) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | last(v2) = v0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | elem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v2) | ordered(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v2) | ? [v3] : ? [v4] : (pidMsg(v0) = v3 & host(v3) = v4 & ! [v5] : ! [v6] : ( ~ (pidMsg(v5) = v6) | ~ pidElem(v5) | ~ pidElem(v0) | ~ elem(v5, v1) | leq(v3, v6) | ? [v7] : ( ~ (v7 = v4) & host(v6) = v7)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v1) | ordered(v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (pidMsg(v5) = v6 & pidMsg(v0) = v3 & host(v6) = v4 & host(v3) = v4 & pidElem(v5) & pidElem(v0) & elem(v5, v1) & ~ leq(v3, v6))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | tail(v2) = v1) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | head(v2) = v0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | elem(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v1) = v2) | ~ (m_Ldr(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v1) = v2) | ~ (m_Down(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v0) = v2) | ~ (m_NotNorm(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v0) = v2) | ~ (m_Halt(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v1) = v2) | ~ (m_Down(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v0) = v2) | ~ (m_NotNorm(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v0) = v2) | ~ (m_Halt(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v1) = v2) | ~ (m_Down(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v0) = v2) | ~ (m_Halt(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v0) = v2) | ~ (host(v1) = nbr_proc) | ~ elem(v2, all_0_1_1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Down(v0) = v2) | ~ (m_Halt(v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (s(v1) = v2) | ~ leq(v0, v1) | leq(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ack(v0, v1) = v2) | setIn(v1, pids) | ? [v3] : ? [v4] : (host(v0) = v3 & queue(v3) = v4 & ~ elem(v2, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ack(v0, v1) = v2) | setIn(v0, pids) | ? [v3] : ? [v4] : (host(v0) = v3 & queue(v3) = v4 & ~ elem(v2, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (host(v1) = v2) | ~ (host(v0) = v2) | ? [v3] : ( ~ (v3 = v2) & s(v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ leq(v0, v1) | leq(v0, v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ leq(v1, v0) | ~ leq(v0, v1)) & ! [v0] : ! [v1] : ~ (snoc(v1, v0) = q_nil) & ! [v0] : ! [v1] : ( ~ (snoc(q_nil, v0) = v1) | ordered(v1)) & ! [v0] : ! [v1] : ~ (cons(v0, v1) = q_nil) & ! [v0] : ! [v1] : ( ~ (cons(v0, q_nil) = v1) | snoc(q_nil, v0) = v1) & ! [v0] : ! [v1] : ( ~ (cons(v0, q_nil) = v1) | ordered(v1)) & ! [v0] : ! [v1] : ( ~ (m_Down(v1) = v0) | pidElem(v0)) & ! [v0] : ! [v1] : ( ~ (m_Down(v0) = v1) | pidMsg(v1) = v0) & ! [v0] : ! [v1] : ( ~ (m_Halt(v1) = v0) | pidElem(v0)) & ! [v0] : ! [v1] : ( ~ (m_Halt(v0) = v1) | pidMsg(v1) = v0) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | leq(v0, v0)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ leq(v1, v0)) & ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | ~ setIn(v0, alive) | ? [v2] : ((v2 = v0 & index(elid, v1) = v0) | ( ~ (v2 = elec_1) & ~ (v2 = elec_2) & index(status, v1) = v2))) & ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | leq(v1, nbr_proc)) & ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | leq(all_0_19_19, v1)) & ! [v0] : (v0 = all_0_3_3 | ~ leq(all_0_19_19, v0) | leq(nbr_proc, v0) | setIn(v0, all_0_4_4)) & ! [v0] : ( ~ pidElem(v0) | ? [v1] : ? [v2] : ((v2 = v0 & m_Down(v1) = v0) | (v2 = v0 & m_Halt(v1) = v0))) & ! [v0] : ~ setIn(v0, setEmpty) & ! [v0] : ~ elem(v0, q_nil) & ? [v0] : ? [v1] : ? [v2] : index(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : snoc(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : cons(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : m_Ack(v1, v0) = v2 & ? [v0] : ? [v1] : pidMsg(v0) = v1 & ? [v0] : ? [v1] : init(v0) = v1 & ? [v0] : ? [v1] : last(v0) = v1 & ? [v0] : ? [v1] : tail(v0) = v1 & ? [v0] : ? [v1] : head(v0) = v1 & ? [v0] : ? [v1] : m_NormQ(v0) = v1 & ? [v0] : ? [v1] : m_Ldr(v0) = v1 & ? [v0] : ? [v1] : m_NotNorm(v0) = v1 & ? [v0] : ? [v1] : m_Down(v0) = v1 & ? [v0] : ? [v1] : m_Halt(v0) = v1 & ? [v0] : ? [v1] : s(v0) = v1 & ? [v0] : ? [v1] : host(v0) = v1 & ? [v0] : ? [v1] : queue(v0) = v1 & ? [v0] : ? [v1] : (leq(v1, v0) | leq(v0, v1)) & ? [v0] : leq(v0, v0) % 251.65/184.33 | % 251.65/184.33 | Applying alpha-rule on (1) yields: % 251.65/184.33 | (2) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (host(v0) = v2) | ~ (host(v0) = v1)) % 251.65/184.33 | (3) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Down(v0) = v2) | ~ (m_Down(v0) = v1)) % 251.65/184.33 | (4) ? [v0] : ? [v1] : m_NormQ(v0) = v1 % 251.65/184.34 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_NormQ(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) % 251.65/184.34 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (head(v2) = v1) | ~ (head(v2) = v0)) % 251.82/184.34 | (7) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NotNorm(v2) = v1) | ~ (m_NotNorm(v2) = v0)) % 251.82/184.34 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Halt(v2) = v1) | ~ (m_Halt(v2) = v0)) % 251.82/184.34 | (9) ~ setIn(nil, alive) % 251.82/184.34 | (10) elem(all_0_2_2, all_0_1_1) % 251.82/184.34 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v1) = v2) | ~ (m_Down(v0) = v2)) % 251.82/184.34 | (12) m_Ack(all_0_17_17, all_0_15_15) = all_0_12_12 % 251.82/184.34 | (13) ~ (wait = elec_2) % 251.82/184.34 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v1) = v2) | ~ (m_Down(v0) = v2)) % 251.82/184.34 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (s(v1) = v2) | ~ leq(v0, v1) | leq(v0, v2)) % 251.82/184.34 | (16) s(zero) = all_0_19_19 % 251.82/184.34 | (17) ! [v0] : ! [v1] : ( ~ (m_Down(v0) = v1) | pidMsg(v1) = v0) % 251.82/184.34 | (18) ? [v0] : ? [v1] : m_Ldr(v0) = v1 % 251.82/184.34 | (19) ! [v0] : ! [v1] : ( ~ (m_Halt(v0) = v1) | pidMsg(v1) = v0) % 251.82/184.34 | (20) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | leq(v0, v0)) % 251.82/184.34 | (21) ~ (norm = wait) % 251.82/184.34 | (22) host(all_0_7_7) = nbr_proc % 251.82/184.34 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | elem(v0, v2)) % 251.82/184.34 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_NotNorm(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) % 251.82/184.34 | (25) ? [v0] : ? [v1] : pidMsg(v0) = v1 % 251.82/184.34 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NotNorm(v1) = v2) | ~ (m_NotNorm(v0) = v2)) % 251.82/184.34 | (27) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ leq(v1, v0)) % 251.82/184.34 | (28) queue(nbr_proc) = all_0_1_1 % 251.82/184.34 | (29) ? [v0] : ? [v1] : ? [v2] : m_Ack(v1, v0) = v2 % 251.82/184.34 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v0) = v2) | ~ (m_Halt(v1) = v2)) % 251.82/184.34 | (31) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_NormQ(v0) = v2) | ~ (m_NormQ(v0) = v1)) % 251.82/184.34 | (32) ~ leq(nbr_proc, all_0_11_11) % 251.82/184.34 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (m_Down(v0) = v5) | ~ (host(v2) = v3) | ~ (host(v1) = v4) | ~ setIn(v2, alive) | ? [v6] : ? [v7] : (( ~ (v7 = v4) & index(elid, v3) = v6 & host(v6) = v7) | ( ~ (v6 = v3) & host(v0) = v6) | ( ~ (v6 = wait) & index(status, v3) = v6) | (queue(v4) = v6 & ~ elem(v5, v6)))) % 251.82/184.34 | (34) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Down(v1) = v2) | ~ (m_Down(v0) = v2)) % 251.82/184.34 | (35) ? [v0] : ? [v1] : ? [v2] : index(v1, v0) = v2 % 251.82/184.34 | (36) ! [v0] : ! [v1] : ( ~ (cons(v0, q_nil) = v1) | ordered(v1)) % 251.82/184.34 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (cons(v1, v2) = v3) | ~ elem(v0, v2) | elem(v0, v3)) % 251.82/184.34 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Down(v1) = v2) | ~ (host(v0) = v3) | ? [v4] : (( ~ (v4 = v3) & host(v1) = v4) | (queue(v3) = v4 & ~ elem(v2, v4)))) % 251.82/184.34 | (39) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | init(v2) = v1) % 251.82/184.34 | (40) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Down(v0) = v2) | ~ (m_Halt(v1) = v2)) % 251.82/184.34 | (41) ! [v0] : ! [v1] : ( ~ (cons(v0, q_nil) = v1) | snoc(q_nil, v0) = v1) % 251.82/184.34 | (42) ~ (norm = elec_2) % 251.82/184.34 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v0) = v2) | ~ (m_Halt(v1) = v2)) % 251.82/184.34 | (44) ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | leq(all_0_19_19, v1)) % 251.82/184.34 | (45) setIn(all_0_16_16, alive) % 251.82/184.34 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (snoc(v2, v1) = v3) | ~ elem(v0, v2) | elem(v0, v3)) % 251.82/184.34 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cons(v1, v2) = v3) | ~ elem(v0, v3) | elem(v0, v2)) % 251.82/184.34 | (48) ? [v0] : ? [v1] : (leq(v1, v0) | leq(v0, v1)) % 251.82/184.34 | (49) setIn(all_0_8_8, alive) % 251.82/184.34 | (50) ? [v0] : ? [v1] : ? [v2] : snoc(v1, v0) = v2 % 251.82/184.34 | (51) ! [v0] : ! [v1] : ~ (cons(v0, v1) = q_nil) % 251.82/184.34 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (last(v2) = v1) | ~ (last(v2) = v0)) % 251.82/184.34 | (53) s(all_0_11_11) = all_0_14_14 % 251.82/184.34 | (54) ! [v0] : ! [v1] : (v1 = v0 | ~ leq(v1, v0) | ~ leq(v0, v1)) % 251.82/184.34 | (55) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Ldr(v0) = v2) | ~ (m_Ldr(v0) = v1)) % 251.82/184.35 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v0) = v2) | ~ (m_NotNorm(v1) = v2)) % 251.82/184.35 | (57) ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | leq(v1, nbr_proc)) % 251.82/184.35 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (init(v2) = v1) | ~ (init(v2) = v0)) % 251.82/184.35 | (59) ! [v0] : ~ elem(v0, q_nil) % 251.82/184.35 | (60) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_Halt(v0) = v2) | ~ (m_Halt(v0) = v1)) % 251.82/184.35 | (61) ? [v0] : ? [v1] : last(v0) = v1 % 251.82/184.35 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v1) | ordered(v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (pidMsg(v5) = v6 & pidMsg(v0) = v3 & host(v6) = v4 & host(v3) = v4 & pidElem(v5) & pidElem(v0) & elem(v5, v1) & ~ leq(v6, v3))) % 251.82/184.35 | (63) index(down, nbr_proc) = all_0_4_4 % 251.82/184.35 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Ldr(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) % 251.82/184.35 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (m_Down(v2) = v4) | ~ (m_Down(v1) = v5) | ~ (host(v3) = nbr_proc) | ~ (host(v0) = v6) | ~ setIn(v0, alive) | ? [v7] : ? [v8] : ? [v9] : ((v7 = all_0_1_1 & ~ elem(v4, all_0_1_1)) | (v7 = all_0_4_4 & ~ (v9 = v8) & host(v2) = v8 & leq(all_0_19_19, v9) & ~ leq(nbr_proc, v9) & ~ setIn(v9, all_0_4_4)) | ( ~ (v7 = nbr_proc) & host(v1) = v7) | (queue(v6) = v7 & ~ elem(v5, v7)))) % 251.82/184.35 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (snoc(v0, v3) = v4) | ~ (m_Ack(v1, v2) = v3) | ~ ordered(v0) | ordered(v4)) % 251.82/184.35 | (67) ! [v0] : ! [v1] : ~ (snoc(v1, v0) = q_nil) % 251.82/184.35 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (cons(v3, v0) = v4) | ~ (m_Down(v2) = v5) | ~ (m_Halt(v1) = v3) | ~ ordered(v4) | ~ elem(v5, v0) | leq(v1, v2) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & host(v2) = v7 & host(v1) = v6)) % 251.82/184.35 | (69) ? [v0] : ? [v1] : tail(v0) = v1 % 251.82/184.35 | (70) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | tail(v2) = v1) % 251.82/184.35 | (71) ! [v0] : ! [v1] : ( ~ (m_Down(v1) = v0) | pidElem(v0)) % 251.82/184.35 | (72) ! [v0] : ~ setIn(v0, setEmpty) % 251.82/184.35 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (m_Down(v3) = v6) | ~ (m_Down(v1) = v7) | ~ (host(v2) = v4) | ~ (host(v0) = v5) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v8] : (( ~ (v8 = v5) & host(v1) = v8) | ( ~ (v8 = v4) & host(v3) = v8) | (queue(v5) = v8 & ~ elem(v6, v8)) | (queue(v4) = v8 & ~ elem(v7, v8)))) % 251.82/184.35 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v0) = v2) | ~ (m_Halt(v1) = v2)) % 251.82/184.35 | (75) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (host(v2) = v1) | ~ (host(v2) = v0)) % 251.82/184.35 | (76) ! [v0] : ! [v1] : ! [v2] : ( ~ (host(v1) = v2) | ~ (host(v0) = v2) | ? [v3] : ( ~ (v3 = v2) & s(v2) = v3)) % 251.82/184.35 | (77) m_Down(all_0_6_6) = all_0_2_2 % 251.82/184.35 | (78) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v2) | ordered(v1)) % 251.82/184.35 | (79) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (host(v1) = v2) | ~ (host(v0) = v2) | ~ setIn(v1, alive) | ~ setIn(v0, alive)) % 251.82/184.35 | (80) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v1) | ordered(v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (pidMsg(v5) = v6 & pidMsg(v0) = v3 & host(v6) = v4 & host(v3) = v4 & pidElem(v5) & pidElem(v0) & elem(v5, v1) & ~ leq(v3, v6))) % 251.82/184.35 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (m_Ack(v1, v3) = v4) | ~ (m_Ack(v0, v2) = v4)) % 251.82/184.35 | (82) ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ leq(v0, v1) | leq(v0, v2)) % 251.82/184.35 | (83) ~ (elec_1 = elec_2) % 251.82/184.35 | (84) ? [v0] : ? [v1] : head(v0) = v1 % 251.82/184.35 | (85) ? [v0] : ? [v1] : m_Down(v0) = v1 % 251.82/184.35 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Down(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) % 251.82/184.35 | (87) ? [v0] : ? [v1] : queue(v0) = v1 % 251.82/184.35 | (88) ! [v0] : ! [v1] : ( ~ (m_Halt(v1) = v0) | pidElem(v0)) % 251.82/184.35 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) % 251.82/184.35 | (90) ~ (wait = elec_1) % 251.82/184.35 | (91) m_Down(all_0_7_7) = all_0_0_0 % 251.82/184.35 | (92) snoc(all_0_18_18, all_0_10_10) = all_0_9_9 % 251.82/184.36 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Ldr(v2) = v1) | ~ (m_Ldr(v2) = v0)) % 251.82/184.36 | (94) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NormQ(v2) = v1) | ~ (m_NormQ(v2) = v0)) % 251.82/184.36 | (95) ? [v0] : ? [v1] : host(v0) = v1 % 251.82/184.36 | (96) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (snoc(v3, v2) = v1) | ~ (snoc(v3, v2) = v0)) % 251.82/184.36 | (97) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | head(v2) = v0) % 251.82/184.36 | (98) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Ldr(v1) = v2) | ~ (host(v0) = v3) | ? [v4] : ((host(v1) = v4 & ~ leq(v3, v4)) | (queue(v3) = v4 & ~ elem(v2, v4)))) % 251.82/184.36 | (99) ~ (norm = elec_1) % 251.82/184.36 | (100) host(all_0_15_15) = all_0_11_11 % 251.82/184.36 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v1) = v3) | ~ (s(v0) = v2) | ~ leq(v0, v1) | leq(v2, v3)) % 251.82/184.36 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v1) = v3) | ~ (s(v0) = v2) | ~ leq(v2, v3) | leq(v0, v1)) % 251.82/184.36 | (103) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NormQ(v1) = v2) | ~ (m_Ldr(v0) = v2)) % 251.82/184.36 | (104) index(elid, all_0_14_14) = all_0_17_17 % 251.82/184.36 | (105) ! [v0] : ( ~ pidElem(v0) | ? [v1] : ? [v2] : ((v2 = v0 & m_Down(v1) = v0) | (v2 = v0 & m_Halt(v1) = v0))) % 251.82/184.36 | (106) index(status, nbr_proc) = elec_1 % 251.82/184.36 | (107) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | last(v2) = v0) % 251.82/184.36 | (108) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Ldr(v1) = v2) | ~ (m_Ldr(v0) = v2)) % 251.82/184.36 | (109) ! [v0] : ! [v1] : ( ~ (snoc(q_nil, v0) = v1) | ordered(v1)) % 251.82/184.36 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (m_Ack(v3, v2) = v1) | ~ (m_Ack(v3, v2) = v0)) % 251.82/184.36 | (111) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v2) | ordered(v1)) % 251.82/184.36 | (112) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (m_Halt(v2) = v3) | ~ (m_Ack(v0, v1) = v3)) % 251.82/184.36 | (113) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | ~ ordered(v2) | ? [v3] : ? [v4] : (pidMsg(v0) = v3 & host(v3) = v4 & ! [v5] : ! [v6] : ( ~ (pidMsg(v5) = v6) | ~ pidElem(v5) | ~ pidElem(v0) | ~ elem(v5, v1) | leq(v3, v6) | ? [v7] : ( ~ (v7 = v4) & host(v6) = v7)))) % 251.82/184.36 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | v0 = q_nil | ~ (tail(v0) = v2) | ~ (cons(v1, v2) = v3) | ~ (head(v0) = v1)) % 251.82/184.36 | (115) ! [v0] : ! [v1] : ! [v2] : ( ~ (snoc(v1, v0) = v2) | ~ ordered(v2) | ? [v3] : ? [v4] : (pidMsg(v0) = v3 & host(v3) = v4 & ! [v5] : ! [v6] : ( ~ (pidMsg(v5) = v6) | ~ pidElem(v5) | ~ pidElem(v0) | ~ elem(v5, v1) | leq(v6, v3) | ? [v7] : ( ~ (v7 = v4) & host(v6) = v7)))) % 251.82/184.36 | (116) ? [v0] : ? [v1] : m_Halt(v0) = v1 % 251.82/184.36 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (m_Down(v0) = v5) | ~ (host(v2) = v3) | ~ (host(v1) = v4) | ~ setIn(v2, alive) | ? [v6] : (( ~ (v6 = v4) & index(ldr, v3) = v6) | ( ~ (v6 = v3) & host(v0) = v6) | ( ~ (v6 = norm) & index(status, v3) = v6) | (queue(v4) = v6 & ~ elem(v5, v6)))) % 251.82/184.36 | (118) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (queue(v2) = v1) | ~ (queue(v2) = v0)) % 251.82/184.36 | (119) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 251.82/184.36 | (120) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v0) = v2) | ~ (host(v1) = nbr_proc) | ~ elem(v2, all_0_1_1)) % 251.82/184.36 | (121) queue(all_0_14_14) = all_0_13_13 % 251.82/184.36 | (122) ordered(q_nil) % 251.82/184.36 | (123) cons(all_0_12_12, all_0_18_18) = all_0_13_13 % 251.82/184.36 | (124) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (snoc(v2, v1) = v3) | ~ elem(v0, v3) | elem(v0, v2)) % 251.82/184.36 | (125) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (m_NotNorm(v0) = v2) | ~ (m_NotNorm(v0) = v1)) % 251.82/184.36 | (126) ! [v0] : ! [v1] : ! [v2] : ( ~ (cons(v0, v1) = v2) | elem(v0, v2)) % 251.82/184.36 | (127) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ack(v0, v1) = v2) | setIn(v1, pids) | ? [v3] : ? [v4] : (host(v0) = v3 & queue(v3) = v4 & ~ elem(v2, v4))) % 251.82/184.36 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (m_Down(v3) = v6) | ~ (host(v2) = v4) | ~ (host(v1) = v5) | ~ (host(v0) = v5) | ~ setIn(v2, alive) | ~ setIn(v0, alive) | ? [v7] : (( ~ (v7 = v4) & host(v3) = v7) | (index(down, v4) = v7 & ~ setIn(v5, v7)) | (queue(v5) = v7 & ~ elem(v6, v7)))) % 251.82/184.37 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (snoc(v2, v1) = v3) | ~ (cons(v0, v3) = v4) | ? [v5] : (snoc(v5, v1) = v4 & cons(v0, v2) = v5)) % 251.82/184.37 | (130) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (pidMsg(v2) = v1) | ~ (pidMsg(v2) = v0)) % 251.82/184.37 | (131) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ldr(v0) = v2) | ~ (m_NotNorm(v1) = v2)) % 251.82/184.37 | (132) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Down(v2) = v1) | ~ (m_Down(v2) = v0)) % 251.82/184.37 | (133) m_Halt(all_0_16_16) = all_0_10_10 % 251.82/184.37 | (134) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_NotNorm(v1) = v2) | ~ (m_Down(v0) = v2)) % 251.82/184.37 | (135) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | v0 = q_nil | ~ (init(v0) = v1) | ~ (snoc(v1, v2) = v3) | ~ (last(v0) = v2)) % 251.82/184.37 | (136) ! [v0] : ! [v1] : ( ~ (host(v0) = v1) | ~ setIn(v0, alive) | ? [v2] : ((v2 = v0 & index(elid, v1) = v0) | ( ~ (v2 = elec_1) & ~ (v2 = elec_2) & index(status, v1) = v2))) % 251.82/184.37 | (137) ? [v0] : leq(v0, v0) % 251.82/184.37 | (138) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (index(v3, v2) = v1) | ~ (index(v3, v2) = v0)) % 251.82/184.37 | (139) ? [v0] : ? [v1] : m_NotNorm(v0) = v1 % 251.82/184.37 | (140) ! [v0] : ! [v1] : ! [v2] : ( ~ (m_Ack(v0, v1) = v2) | setIn(v0, pids) | ? [v3] : ? [v4] : (host(v0) = v3 & queue(v3) = v4 & ~ elem(v2, v4))) % 251.82/184.37 | (141) host(all_0_6_6) = all_0_3_3 % 251.82/184.37 | (142) ? [v0] : ? [v1] : init(v0) = v1 % 251.82/184.37 | (143) index(pendack, all_0_14_14) = all_0_11_11 % 251.82/184.37 | (144) host(all_0_16_16) = all_0_14_14 % 251.82/184.37 | (145) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (m_Ack(v1, v3) = v4) | ~ (m_Ack(v0, v2) = v4)) % 251.82/184.37 | (146) index(status, all_0_14_14) = elec_2 % 251.82/184.37 | (147) host(all_0_5_5) = nbr_proc % 251.82/184.37 | (148) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (snoc(v0, v2) = v3) | ~ (m_Ldr(v1) = v2) | ~ ordered(v0) | ordered(v3)) % 251.82/184.37 | (149) ! [v0] : (v0 = all_0_3_3 | ~ leq(all_0_19_19, v0) | leq(nbr_proc, v0) | setIn(v0, all_0_4_4)) % 251.82/184.37 | (150) ~ (all_0_14_14 = nbr_proc) % 251.82/184.37 | (151) ? [v0] : ? [v1] : s(v0) = v1 % 251.82/184.37 | (152) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_Halt(v1) = v2) | ~ (m_Halt(v0) = v2)) % 251.82/184.37 | (153) ? [v0] : ? [v1] : ? [v2] : cons(v1, v0) = v2 % 251.82/184.37 | (154) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (tail(v2) = v1) | ~ (tail(v2) = v0)) % 251.82/184.37 | (155) host(all_0_8_8) = all_0_14_14 % 251.82/184.37 | (156) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (s(v1) = v2) | ~ leq(v0, v2) | leq(v0, v1)) % 251.82/184.37 | (157) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (m_NormQ(v1) = v2) | ~ (m_NormQ(v0) = v2)) % 251.82/184.37 | (158) elem(all_0_0_0, all_0_9_9) % 251.82/184.37 | (159) leq(all_0_19_19, nbr_proc) % 251.82/184.37 | % 251.82/184.37 | Instantiating formula (40) with all_0_10_10, all_0_16_16, all_0_7_7 and discharging atoms m_Halt(all_0_16_16) = all_0_10_10, yields: % 251.82/184.37 | (160) ~ (m_Down(all_0_7_7) = all_0_10_10) % 251.82/184.37 | % 251.82/184.37 | Instantiating formula (79) with all_0_14_14, all_0_8_8, all_0_16_16 and discharging atoms host(all_0_8_8) = all_0_14_14, host(all_0_16_16) = all_0_14_14, setIn(all_0_8_8, alive), setIn(all_0_16_16, alive), yields: % 251.82/184.37 | (161) all_0_8_8 = all_0_16_16 % 251.82/184.37 | % 251.82/184.37 | From (161) and (155) follows: % 251.82/184.37 | (144) host(all_0_16_16) = all_0_14_14 % 251.82/184.37 | % 251.82/184.37 | From (161) and (49) follows: % 251.82/184.37 | (45) setIn(all_0_16_16, alive) % 251.82/184.37 | % 251.82/184.37 | Using (91) and (160) yields: % 251.82/184.37 | (164) ~ (all_0_0_0 = all_0_10_10) % 251.82/184.37 | % 251.82/184.37 | Instantiating formula (38) with nbr_proc, all_0_2_2, all_0_6_6, all_0_7_7 and discharging atoms m_Down(all_0_6_6) = all_0_2_2, host(all_0_7_7) = nbr_proc, yields: % 251.82/184.38 | (165) ? [v0] : (( ~ (v0 = nbr_proc) & host(all_0_6_6) = v0) | (queue(nbr_proc) = v0 & ~ elem(all_0_2_2, v0))) % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (38) with nbr_proc, all_0_0_0, all_0_7_7, all_0_7_7 and discharging atoms m_Down(all_0_7_7) = all_0_0_0, host(all_0_7_7) = nbr_proc, yields: % 251.82/184.38 | (166) ? [v0] : (( ~ (v0 = nbr_proc) & host(all_0_7_7) = v0) | (queue(nbr_proc) = v0 & ~ elem(all_0_0_0, v0))) % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (38) with all_0_14_14, all_0_0_0, all_0_7_7, all_0_16_16 and discharging atoms m_Down(all_0_7_7) = all_0_0_0, host(all_0_16_16) = all_0_14_14, yields: % 251.82/184.38 | (167) ? [v0] : (( ~ (v0 = all_0_14_14) & host(all_0_7_7) = v0) | (queue(all_0_14_14) = v0 & ~ elem(all_0_0_0, v0))) % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (65) with all_0_14_14, all_0_0_0, all_0_2_2, all_0_7_7, all_0_6_6, all_0_7_7, all_0_16_16 and discharging atoms m_Down(all_0_6_6) = all_0_2_2, m_Down(all_0_7_7) = all_0_0_0, host(all_0_7_7) = nbr_proc, host(all_0_16_16) = all_0_14_14, setIn(all_0_16_16, alive), yields: % 251.82/184.38 | (168) ? [v0] : ? [v1] : ? [v2] : ((v0 = all_0_1_1 & ~ elem(all_0_2_2, all_0_1_1)) | (v0 = all_0_4_4 & ~ (v2 = v1) & host(all_0_6_6) = v1 & leq(all_0_19_19, v2) & ~ leq(nbr_proc, v2) & ~ setIn(v2, all_0_4_4)) | ( ~ (v0 = nbr_proc) & host(all_0_7_7) = v0) | (queue(all_0_14_14) = v0 & ~ elem(all_0_0_0, v0))) % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (37) with all_0_13_13, all_0_18_18, all_0_12_12, all_0_0_0 and discharging atoms cons(all_0_12_12, all_0_18_18) = all_0_13_13, yields: % 251.82/184.38 | (169) ~ elem(all_0_0_0, all_0_18_18) | elem(all_0_0_0, all_0_13_13) % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (124) with all_0_9_9, all_0_18_18, all_0_10_10, all_0_0_0 and discharging atoms snoc(all_0_18_18, all_0_10_10) = all_0_9_9, elem(all_0_0_0, all_0_9_9), yields: % 251.82/184.38 | (170) all_0_0_0 = all_0_10_10 | elem(all_0_0_0, all_0_18_18) % 251.82/184.38 | % 251.82/184.38 | Instantiating (168) with all_60_0_73, all_60_1_74, all_60_2_75 yields: % 251.82/184.38 | (171) (all_60_2_75 = all_0_1_1 & ~ elem(all_0_2_2, all_0_1_1)) | (all_60_2_75 = all_0_4_4 & ~ (all_60_0_73 = all_60_1_74) & host(all_0_6_6) = all_60_1_74 & leq(all_0_19_19, all_60_0_73) & ~ leq(nbr_proc, all_60_0_73) & ~ setIn(all_60_0_73, all_0_4_4)) | ( ~ (all_60_2_75 = nbr_proc) & host(all_0_7_7) = all_60_2_75) | (queue(all_0_14_14) = all_60_2_75 & ~ elem(all_0_0_0, all_60_2_75)) % 251.82/184.38 | % 251.82/184.38 | Instantiating (167) with all_65_0_81 yields: % 251.82/184.38 | (172) ( ~ (all_65_0_81 = all_0_14_14) & host(all_0_7_7) = all_65_0_81) | (queue(all_0_14_14) = all_65_0_81 & ~ elem(all_0_0_0, all_65_0_81)) % 251.82/184.38 | % 251.82/184.38 | Instantiating (166) with all_88_0_108 yields: % 251.82/184.38 | (173) ( ~ (all_88_0_108 = nbr_proc) & host(all_0_7_7) = all_88_0_108) | (queue(nbr_proc) = all_88_0_108 & ~ elem(all_0_0_0, all_88_0_108)) % 251.82/184.38 | % 251.82/184.38 | Instantiating (165) with all_92_0_112 yields: % 251.82/184.38 | (174) ( ~ (all_92_0_112 = nbr_proc) & host(all_0_6_6) = all_92_0_112) | (queue(nbr_proc) = all_92_0_112 & ~ elem(all_0_2_2, all_92_0_112)) % 251.82/184.38 | % 251.82/184.38 +-Applying beta-rule and splitting (173), into two cases. % 251.82/184.38 |-Branch one: % 251.82/184.38 | (175) ~ (all_88_0_108 = nbr_proc) & host(all_0_7_7) = all_88_0_108 % 251.82/184.38 | % 251.82/184.38 | Applying alpha-rule on (175) yields: % 251.82/184.38 | (176) ~ (all_88_0_108 = nbr_proc) % 251.82/184.38 | (177) host(all_0_7_7) = all_88_0_108 % 251.82/184.38 | % 251.82/184.38 +-Applying beta-rule and splitting (170), into two cases. % 251.82/184.38 |-Branch one: % 251.82/184.38 | (178) elem(all_0_0_0, all_0_18_18) % 251.82/184.38 | % 251.82/184.38 +-Applying beta-rule and splitting (169), into two cases. % 251.82/184.38 |-Branch one: % 251.82/184.38 | (179) ~ elem(all_0_0_0, all_0_18_18) % 251.82/184.38 | % 251.82/184.38 | Using (178) and (179) yields: % 251.82/184.38 | (180) $false % 251.82/184.38 | % 251.82/184.38 |-The branch is then unsatisfiable % 251.82/184.38 |-Branch two: % 251.82/184.38 | (178) elem(all_0_0_0, all_0_18_18) % 251.82/184.38 | (182) elem(all_0_0_0, all_0_13_13) % 251.82/184.38 | % 251.82/184.38 +-Applying beta-rule and splitting (172), into two cases. % 251.82/184.38 |-Branch one: % 251.82/184.38 | (183) ~ (all_65_0_81 = all_0_14_14) & host(all_0_7_7) = all_65_0_81 % 251.82/184.38 | % 251.82/184.38 | Applying alpha-rule on (183) yields: % 251.82/184.38 | (184) ~ (all_65_0_81 = all_0_14_14) % 251.82/184.38 | (185) host(all_0_7_7) = all_65_0_81 % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (2) with all_88_0_108, nbr_proc, all_0_7_7 and discharging atoms host(all_0_7_7) = all_88_0_108, host(all_0_7_7) = nbr_proc, yields: % 251.82/184.38 | (186) all_88_0_108 = nbr_proc % 251.82/184.38 | % 251.82/184.38 | Instantiating formula (2) with all_65_0_81, all_88_0_108, all_0_7_7 and discharging atoms host(all_0_7_7) = all_88_0_108, host(all_0_7_7) = all_65_0_81, yields: % 251.82/184.38 | (187) all_88_0_108 = all_65_0_81 % 251.82/184.38 | % 251.82/184.38 | Combining equations (186,187) yields a new equation: % 251.82/184.38 | (188) all_65_0_81 = nbr_proc % 251.82/184.38 | % 251.82/184.38 | Combining equations (188,187) yields a new equation: % 251.82/184.38 | (186) all_88_0_108 = nbr_proc % 251.82/184.38 | % 251.82/184.38 | Equations (186) can reduce 176 to: % 251.82/184.38 | (190) $false % 251.82/184.38 | % 251.82/184.38 |-The branch is then unsatisfiable % 251.82/184.38 |-Branch two: % 251.82/184.38 | (191) queue(all_0_14_14) = all_65_0_81 & ~ elem(all_0_0_0, all_65_0_81) % 251.82/184.38 | % 251.82/184.38 | Applying alpha-rule on (191) yields: % 251.82/184.38 | (192) queue(all_0_14_14) = all_65_0_81 % 251.82/184.38 | (193) ~ elem(all_0_0_0, all_65_0_81) % 251.82/184.38 | % 251.82/184.39 | Instantiating formula (118) with all_0_14_14, all_65_0_81, all_0_13_13 and discharging atoms queue(all_0_14_14) = all_65_0_81, queue(all_0_14_14) = all_0_13_13, yields: % 251.82/184.39 | (194) all_65_0_81 = all_0_13_13 % 251.82/184.39 | % 251.82/184.39 | Using (182) and (193) yields: % 251.82/184.39 | (195) ~ (all_65_0_81 = all_0_13_13) % 251.82/184.39 | % 251.82/184.39 | Equations (194) can reduce 195 to: % 251.82/184.39 | (190) $false % 251.82/184.39 | % 251.82/184.39 |-The branch is then unsatisfiable % 251.82/184.39 |-Branch two: % 251.82/184.39 | (179) ~ elem(all_0_0_0, all_0_18_18) % 251.82/184.39 | (198) all_0_0_0 = all_0_10_10 % 251.82/184.39 | % 251.82/184.39 | Equations (198) can reduce 164 to: % 251.82/184.39 | (190) $false % 251.82/184.39 | % 251.82/184.39 |-The branch is then unsatisfiable % 251.82/184.39 |-Branch two: % 251.82/184.39 | (200) queue(nbr_proc) = all_88_0_108 & ~ elem(all_0_0_0, all_88_0_108) % 251.82/184.39 | % 251.82/184.39 | Applying alpha-rule on (200) yields: % 251.82/184.39 | (201) queue(nbr_proc) = all_88_0_108 % 251.82/184.39 | (202) ~ elem(all_0_0_0, all_88_0_108) % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (170), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (178) elem(all_0_0_0, all_0_18_18) % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (169), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (179) ~ elem(all_0_0_0, all_0_18_18) % 251.82/184.39 | % 251.82/184.39 | Using (178) and (179) yields: % 251.82/184.39 | (180) $false % 251.82/184.39 | % 251.82/184.39 |-The branch is then unsatisfiable % 251.82/184.39 |-Branch two: % 251.82/184.39 | (178) elem(all_0_0_0, all_0_18_18) % 251.82/184.39 | (182) elem(all_0_0_0, all_0_13_13) % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (172), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (183) ~ (all_65_0_81 = all_0_14_14) & host(all_0_7_7) = all_65_0_81 % 251.82/184.39 | % 251.82/184.39 | Applying alpha-rule on (183) yields: % 251.82/184.39 | (184) ~ (all_65_0_81 = all_0_14_14) % 251.82/184.39 | (185) host(all_0_7_7) = all_65_0_81 % 251.82/184.39 | % 251.82/184.39 | Instantiating formula (2) with all_65_0_81, nbr_proc, all_0_7_7 and discharging atoms host(all_0_7_7) = all_65_0_81, host(all_0_7_7) = nbr_proc, yields: % 251.82/184.39 | (188) all_65_0_81 = nbr_proc % 251.82/184.39 | % 251.82/184.39 | Instantiating formula (118) with nbr_proc, all_88_0_108, all_0_1_1 and discharging atoms queue(nbr_proc) = all_88_0_108, queue(nbr_proc) = all_0_1_1, yields: % 251.82/184.39 | (212) all_88_0_108 = all_0_1_1 % 251.82/184.39 | % 251.82/184.39 | From (188) and (185) follows: % 251.82/184.39 | (22) host(all_0_7_7) = nbr_proc % 251.82/184.39 | % 251.82/184.39 | From (212) and (201) follows: % 251.82/184.39 | (28) queue(nbr_proc) = all_0_1_1 % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (171), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (215) (all_60_2_75 = all_0_1_1 & ~ elem(all_0_2_2, all_0_1_1)) | (all_60_2_75 = all_0_4_4 & ~ (all_60_0_73 = all_60_1_74) & host(all_0_6_6) = all_60_1_74 & leq(all_0_19_19, all_60_0_73) & ~ leq(nbr_proc, all_60_0_73) & ~ setIn(all_60_0_73, all_0_4_4)) | ( ~ (all_60_2_75 = nbr_proc) & host(all_0_7_7) = all_60_2_75) % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (215), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (216) (all_60_2_75 = all_0_1_1 & ~ elem(all_0_2_2, all_0_1_1)) | (all_60_2_75 = all_0_4_4 & ~ (all_60_0_73 = all_60_1_74) & host(all_0_6_6) = all_60_1_74 & leq(all_0_19_19, all_60_0_73) & ~ leq(nbr_proc, all_60_0_73) & ~ setIn(all_60_0_73, all_0_4_4)) % 251.82/184.39 | % 251.82/184.39 +-Applying beta-rule and splitting (216), into two cases. % 251.82/184.39 |-Branch one: % 251.82/184.39 | (217) all_60_2_75 = all_0_1_1 & ~ elem(all_0_2_2, all_0_1_1) % 251.82/184.39 | % 251.82/184.39 | Applying alpha-rule on (217) yields: % 251.82/184.39 | (218) all_60_2_75 = all_0_1_1 % 251.82/184.39 | (219) ~ elem(all_0_2_2, all_0_1_1) % 251.82/184.39 | % 251.82/184.39 | Using (10) and (219) yields: % 251.82/184.39 | (180) $false % 251.82/184.39 | % 251.82/184.39 |-The branch is then unsatisfiable % 251.82/184.39 |-Branch two: % 251.82/184.39 | (221) all_60_2_75 = all_0_4_4 & ~ (all_60_0_73 = all_60_1_74) & host(all_0_6_6) = all_60_1_74 & leq(all_0_19_19, all_60_0_73) & ~ leq(nbr_proc, all_60_0_73) & ~ setIn(all_60_0_73, all_0_4_4) % 251.82/184.39 | % 251.82/184.39 | Applying alpha-rule on (221) yields: % 251.82/184.39 | (222) all_60_2_75 = all_0_4_4 % 251.82/184.39 | (223) ~ (all_60_0_73 = all_60_1_74) % 251.82/184.39 | (224) host(all_0_6_6) = all_60_1_74 % 251.82/184.39 | (225) ~ setIn(all_60_0_73, all_0_4_4) % 251.82/184.39 | (226) leq(all_0_19_19, all_60_0_73) % 251.82/184.39 | (227) ~ leq(nbr_proc, all_60_0_73) % 251.82/184.40 | % 251.82/184.40 +-Applying beta-rule and splitting (174), into two cases. % 251.82/184.40 |-Branch one: % 251.82/184.40 | (228) ~ (all_92_0_112 = nbr_proc) & host(all_0_6_6) = all_92_0_112 % 251.82/184.40 | % 251.82/184.40 | Applying alpha-rule on (228) yields: % 251.82/184.40 | (229) ~ (all_92_0_112 = nbr_proc) % 251.82/184.40 | (230) host(all_0_6_6) = all_92_0_112 % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (2) with all_92_0_112, all_0_3_3, all_0_6_6 and discharging atoms host(all_0_6_6) = all_92_0_112, host(all_0_6_6) = all_0_3_3, yields: % 251.82/184.40 | (231) all_92_0_112 = all_0_3_3 % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (2) with all_60_1_74, all_92_0_112, all_0_6_6 and discharging atoms host(all_0_6_6) = all_92_0_112, host(all_0_6_6) = all_60_1_74, yields: % 251.82/184.40 | (232) all_92_0_112 = all_60_1_74 % 251.82/184.40 | % 251.82/184.40 | Combining equations (231,232) yields a new equation: % 251.82/184.40 | (233) all_60_1_74 = all_0_3_3 % 251.82/184.40 | % 251.82/184.40 | Equations (233) can reduce 223 to: % 251.82/184.40 | (234) ~ (all_60_0_73 = all_0_3_3) % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (149) with all_60_0_73 and discharging atoms leq(all_0_19_19, all_60_0_73), ~ leq(nbr_proc, all_60_0_73), ~ setIn(all_60_0_73, all_0_4_4), yields: % 251.82/184.40 | (235) all_60_0_73 = all_0_3_3 % 251.82/184.40 | % 251.82/184.40 | Equations (235) can reduce 234 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 |-Branch two: % 251.82/184.40 | (237) queue(nbr_proc) = all_92_0_112 & ~ elem(all_0_2_2, all_92_0_112) % 251.82/184.40 | % 251.82/184.40 | Applying alpha-rule on (237) yields: % 251.82/184.40 | (238) queue(nbr_proc) = all_92_0_112 % 251.82/184.40 | (239) ~ elem(all_0_2_2, all_92_0_112) % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (118) with nbr_proc, all_92_0_112, all_0_1_1 and discharging atoms queue(nbr_proc) = all_92_0_112, queue(nbr_proc) = all_0_1_1, yields: % 251.82/184.40 | (240) all_92_0_112 = all_0_1_1 % 251.82/184.40 | % 251.82/184.40 | Using (10) and (239) yields: % 251.82/184.40 | (241) ~ (all_92_0_112 = all_0_1_1) % 251.82/184.40 | % 251.82/184.40 | Equations (240) can reduce 241 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 |-Branch two: % 251.82/184.40 | (243) ~ (all_60_2_75 = nbr_proc) & host(all_0_7_7) = all_60_2_75 % 251.82/184.40 | % 251.82/184.40 | Applying alpha-rule on (243) yields: % 251.82/184.40 | (244) ~ (all_60_2_75 = nbr_proc) % 251.82/184.40 | (245) host(all_0_7_7) = all_60_2_75 % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (2) with all_60_2_75, nbr_proc, all_0_7_7 and discharging atoms host(all_0_7_7) = all_60_2_75, host(all_0_7_7) = nbr_proc, yields: % 251.82/184.40 | (246) all_60_2_75 = nbr_proc % 251.82/184.40 | % 251.82/184.40 | Equations (246) can reduce 244 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 |-Branch two: % 251.82/184.40 | (248) queue(all_0_14_14) = all_60_2_75 & ~ elem(all_0_0_0, all_60_2_75) % 251.82/184.40 | % 251.82/184.40 | Applying alpha-rule on (248) yields: % 251.82/184.40 | (249) queue(all_0_14_14) = all_60_2_75 % 251.82/184.40 | (250) ~ elem(all_0_0_0, all_60_2_75) % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (118) with all_0_14_14, all_60_2_75, all_0_13_13 and discharging atoms queue(all_0_14_14) = all_60_2_75, queue(all_0_14_14) = all_0_13_13, yields: % 251.82/184.40 | (251) all_60_2_75 = all_0_13_13 % 251.82/184.40 | % 251.82/184.40 | Using (182) and (250) yields: % 251.82/184.40 | (252) ~ (all_60_2_75 = all_0_13_13) % 251.82/184.40 | % 251.82/184.40 | Equations (251) can reduce 252 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 |-Branch two: % 251.82/184.40 | (191) queue(all_0_14_14) = all_65_0_81 & ~ elem(all_0_0_0, all_65_0_81) % 251.82/184.40 | % 251.82/184.40 | Applying alpha-rule on (191) yields: % 251.82/184.40 | (192) queue(all_0_14_14) = all_65_0_81 % 251.82/184.40 | (193) ~ elem(all_0_0_0, all_65_0_81) % 251.82/184.40 | % 251.82/184.40 | Instantiating formula (118) with all_0_14_14, all_65_0_81, all_0_13_13 and discharging atoms queue(all_0_14_14) = all_65_0_81, queue(all_0_14_14) = all_0_13_13, yields: % 251.82/184.40 | (194) all_65_0_81 = all_0_13_13 % 251.82/184.40 | % 251.82/184.40 | Using (182) and (193) yields: % 251.82/184.40 | (195) ~ (all_65_0_81 = all_0_13_13) % 251.82/184.40 | % 251.82/184.40 | Equations (194) can reduce 195 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 |-Branch two: % 251.82/184.40 | (179) ~ elem(all_0_0_0, all_0_18_18) % 251.82/184.40 | (198) all_0_0_0 = all_0_10_10 % 251.82/184.40 | % 251.82/184.40 | Equations (198) can reduce 164 to: % 251.82/184.40 | (190) $false % 251.82/184.40 | % 251.82/184.40 |-The branch is then unsatisfiable % 251.82/184.40 % SZS output end Proof for theBenchmark % 251.82/184.40 % 251.82/184.40 183781ms %------------------------------------------------------------------------------