%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV457+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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 21:43:10 EDT 2022 % Result : Theorem 156.72s 156.95s % Output : Refutation 159.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV457+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n011.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 : 600 % 0.12/0.33 % DateTime : Wed Jun 15 09:50:50 EDT 2022 % 0.12/0.34 % CPUTime : % 156.72/156.95 % 156.72/156.95 SPASS V 3.9 % 156.72/156.95 SPASS beiseite: Proof found. % 156.72/156.95 % SZS status Theorem % 156.72/156.95 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 156.72/156.95 SPASS derived 72622 clauses, backtracked 4052 clauses, performed 37 splits and kept 28120 clauses. % 156.72/156.95 SPASS allocated 152900 KBytes. % 156.72/156.95 SPASS spent 0:2:36.52 on the problem. % 156.72/156.95 0:00:00.04 for the input. % 156.72/156.95 0:00:00.05 for the FLOTTER CNF translation. % 156.72/156.95 0:00:01.10 for inferences. % 156.72/156.95 0:00:02.37 for the backtracking. % 156.72/156.95 0:2:31.99 for the reduction. % 156.72/156.95 % 156.72/156.95 % 156.72/156.95 Here is a proof with depth 5, length 168 : % 156.72/156.95 % SZS output start Refutation % 156.72/156.95 2[0:Inp] || -> setIn(skc10,alive)*. % 156.72/156.95 3[0:Inp] || -> setIn(skc9,alive)*. % 156.72/156.95 7[0:Inp] || -> leq(host(u),nbr_proc)*l. % 156.72/156.95 8[0:Inp] || equal(elec_2,elec_1)** -> . % 156.72/156.95 17[0:Inp] || -> ordered(snoc(q_nil,u))*. % 156.72/156.95 21[0:Inp] || -> equal(host(skc10),host(skc7))**. % 156.72/156.95 26[0:Inp] || leq(s(u),u)*l -> . % 156.72/156.95 27[0:Inp] || equal(host(skc9),host(skc6))** -> . % 156.72/156.95 28[0:Inp] || -> equal(index(status__dfg,host(skc10)),elec_2)**. % 156.72/156.95 29[0:Inp] || -> leq(nbr_proc,index(pendack,host(skc10)))*r. % 156.72/156.95 31[0:Inp] || -> equal(index(status__dfg,host(skc9)),norm)**. % 156.72/156.95 32[0:Inp] || equal(m_NotNorm(u),m_Halt(v))* -> . % 156.72/156.95 35[0:Inp] || equal(m_Down(u),m_NotNorm(v))* -> . % 156.72/156.95 42[0:Inp] || -> equal(head(cons(u,v)),u)**. % 156.72/156.95 44[0:Inp] || -> equal(last(snoc(u,v)),v)**. % 156.72/156.95 46[0:Inp] || equal(cons(u,v),q_nil)** -> . % 156.72/156.95 48[0:Inp] || -> leq(u,v)* leq(v,u)*. % 156.72/156.95 49[0:Inp] || -> equal(index(pendack,host(skc10)),host(skc11))**. % 156.72/156.95 50[0:Inp] || -> equal(index(ldr,host(skc9)),host(skc9))**. % 156.72/156.95 56[0:Inp] || -> equal(cons(u,q_nil),snoc(q_nil,u))**. % 156.72/156.95 59[0:Inp] || ordered(cons(u,v))* -> ordered(v). % 156.72/156.95 62[0:Inp] || equal(u,v)* -> leq(v,u). % 156.72/156.95 63[0:Inp] || -> equal(cons(m_Halt(skc7),skc8),queue(host(skc6)))**. % 156.72/156.95 64[0:Inp] ordered(u) || -> ordered(snoc(u,m_Ldr(v)))*. % 156.72/156.95 65[0:Inp] || leq(u,v)*+ -> leq(u,s(v))*. % 156.72/156.95 76[0:Inp] || equal(u,v) -> elem(u,cons(v,w))*. % 156.72/156.95 77[0:Inp] || elem(u,v) -> elem(u,cons(w,v))*. % 156.72/156.95 78[0:Inp] || equal(u,v) -> elem(u,snoc(w,v))*. % 156.72/156.95 80[0:Inp] ordered(u) || -> pidElem(v) ordered(cons(v,u))*. % 156.72/156.95 82[0:Inp] ordered(u) || -> ordered(snoc(u,m_Ack(v,w)))*. % 156.72/156.95 83[0:Inp] || leq(u,v) -> leq(s(u),s(v))*. % 156.72/156.95 86[0:Inp] || -> equal(u,q_nil) equal(cons(head(u),tail(u)),u)**. % 156.72/156.95 87[0:Inp] || -> equal(u,q_nil) equal(snoc(init(u),last(u)),u)**. % 156.72/156.95 88[0:Inp] || -> elem(m_Ack(skc10,skc11),snoc(queue(host(skc10)),m_Ack(skc7,skc6)))*. % 156.72/156.95 91[0:Inp] || elem(m_Ack(u,v),queue(host(u)))* -> setIn(u,pids). % 156.72/156.95 92[0:Inp] || elem(m_Ack(u,v),queue(host(u)))* -> setIn(v,pids). % 156.72/156.95 93[0:Inp] || equal(m_Ack(u,v),m_Ack(w,x))* -> equal(u,w). % 156.72/156.95 94[0:Inp] || equal(m_Ack(u,v),m_Ack(w,x))* -> equal(v,x). % 156.72/156.95 95[0:Inp] || -> equal(cons(u,snoc(v,w)),snoc(cons(u,v),w))**. % 156.72/156.95 96[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 156.72/156.95 97[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 156.72/156.95 98[0:Inp] || elem(u,cons(v,w))* -> equal(u,v) elem(u,w). % 156.72/156.95 99[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 156.72/156.95 102[0:Inp] || leq(u,s(v))* -> leq(u,v) equal(u,s(v)). % 156.72/156.95 105[0:Inp] pidElem(u) || -> equal(m_Down(skf5(u)),u) equal(m_Halt(skf4(u)),u)**. % 156.72/156.95 124[0:Inp] || setIn(u,alive) setIn(v,alive) elem(m_Halt(v),queue(host(w)))* equal(index(status__dfg,host(u)),norm) equal(index(status__dfg,host(v)),elec_2) equal(index(ldr,host(u)),host(u))**+ -> leq(index(pendack,host(v)),host(u))*. % 156.72/156.95 125[0:Inp] || equal(host(u),index(pendack,host(v))) elem(m_Ack(v,u),queue(host(v)))* setIn(v,alive) leq(nbr_proc,index(pendack,host(v))) equal(index(status__dfg,host(v)),elec_2) setIn(w,alive) equal(index(ldr,host(w)),host(w))** equal(index(status__dfg,host(w)),norm) -> . % 156.72/156.95 127[0:Rew:21.0,28.0] || -> equal(index(status__dfg,host(skc7)),elec_2)**. % 156.72/156.95 129[0:Rew:21.0,49.0] || -> equal(index(pendack,host(skc7)),host(skc11))**. % 156.72/156.95 130[0:Rew:21.0,88.0] || -> elem(m_Ack(skc10,skc11),snoc(queue(host(skc7)),m_Ack(skc7,skc6)))*. % 156.72/156.95 131[0:Rew:129.0,29.0,21.0,29.0] || -> leq(nbr_proc,host(skc11))*r. % 156.72/156.95 168[0:Res:2.0,124.1] || elem(m_Halt(skc10),queue(host(u)))* equal(index(status__dfg,host(skc10)),elec_2) setIn(v,alive) equal(index(ldr,host(v)),host(v))** equal(index(status__dfg,host(v)),norm) -> leq(index(pendack,host(skc10)),host(v)). % 156.72/156.95 286[0:Res:96.2,27.0] || leq(host(skc9),host(skc6))*l leq(host(skc6),host(skc9)) -> . % 156.72/156.95 297[0:Res:50.0,125.6] || equal(host(u),index(pendack,host(v))) elem(m_Ack(v,u),queue(host(v)))* setIn(v,alive) leq(nbr_proc,index(pendack,host(v))) equal(index(status__dfg,host(v)),elec_2) setIn(skc9,alive) equal(index(status__dfg,host(skc9)),norm) -> . % 156.72/156.95 348[0:Res:131.0,96.1] || leq(host(skc11),nbr_proc)*l -> equal(host(skc11),nbr_proc). % 156.72/156.95 358[0:Res:130.0,99.0] || -> elem(m_Ack(skc10,skc11),queue(host(skc7)))* equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6)). % 156.72/156.95 452[0:MRR:348.0,7.0] || -> equal(host(skc11),nbr_proc)**. % 156.72/156.95 453[0:Rew:452.0,129.0] || -> equal(index(pendack,host(skc7)),nbr_proc)**. % 156.72/156.95 485[0:Rew:453.0,168.5,21.0,168.5,127.0,168.1,21.0,168.1] || elem(m_Halt(skc10),queue(host(u)))* equal(elec_2,elec_2) setIn(v,alive) equal(index(ldr,host(v)),host(v))** equal(index(status__dfg,host(v)),norm) -> leq(nbr_proc,host(v)). % 156.72/156.95 486[0:Obv:485.1] || setIn(u,alive) elem(m_Halt(skc10),queue(host(v)))* equal(index(status__dfg,host(u)),norm) equal(index(ldr,host(u)),host(u))**+ -> leq(nbr_proc,host(u)). % 156.72/156.95 491[0:Rew:31.0,297.6] || equal(host(u),index(pendack,host(v))) elem(m_Ack(v,u),queue(host(v)))* setIn(v,alive) leq(nbr_proc,index(pendack,host(v))) equal(index(status__dfg,host(v)),elec_2) setIn(skc9,alive) equal(norm,norm) -> . % 156.72/156.95 492[0:Obv:491.6] || equal(host(u),index(pendack,host(v))) elem(m_Ack(v,u),queue(host(v)))* setIn(v,alive) leq(nbr_proc,index(pendack,host(v))) equal(index(status__dfg,host(v)),elec_2) setIn(skc9,alive) -> . % 156.72/156.95 493[0:MRR:492.5,3.0] || setIn(u,alive) leq(nbr_proc,index(pendack,host(u))) equal(host(v),index(pendack,host(u))) elem(m_Ack(u,v),queue(host(u)))* equal(index(status__dfg,host(u)),elec_2) -> . % 156.72/156.95 534[0:SpR:63.0,42.0] || -> equal(head(queue(host(skc6))),m_Halt(skc7))**. % 156.72/156.95 536[0:SpL:63.0,46.0] || equal(queue(host(skc6)),q_nil)** -> . % 156.72/156.95 739[0:SpR:63.0,77.1] || elem(u,skc8) -> elem(u,queue(host(skc6)))*. % 156.72/156.95 765[0:SpR:87.1,78.1] || equal(u,last(v)) -> equal(v,q_nil) elem(u,v)*. % 156.72/156.95 780[0:SpR:86.1,76.1] || equal(u,head(v)) -> equal(v,q_nil) elem(u,v)*. % 156.72/156.95 834[0:Res:739.1,91.0] || elem(m_Ack(skc6,u),skc8)* -> setIn(skc6,pids). % 156.72/156.95 840[0:SpL:21.0,92.0] || elem(m_Ack(skc10,u),queue(host(skc7)))* -> setIn(u,pids). % 156.72/156.95 847[0:SpR:95.0,80.2] ordered(snoc(u,v)) || -> pidElem(w) ordered(snoc(cons(w,u),v))*. % 156.72/156.95 855[0:SpL:95.0,59.0] || ordered(snoc(cons(u,v),w))* -> ordered(snoc(v,w)). % 156.72/156.95 1035[0:SpL:105.2,32.0] pidElem(u) || equal(m_NotNorm(v),u)*+ -> equal(m_Down(skf5(u)),u)**. % 156.72/156.95 1140[0:Res:765.2,98.0] || equal(u,last(cons(v,w)))* -> equal(cons(v,w),q_nil) equal(u,v) elem(u,w)*. % 156.72/156.95 1166[0:Res:765.2,834.0] || equal(m_Ack(skc6,u),last(skc8))** -> equal(skc8,q_nil) setIn(skc6,pids). % 156.72/156.95 1171[0:MRR:1140.1,46.0] || equal(u,last(cons(v,w)))*+ -> equal(u,v) elem(u,w)*. % 156.72/156.95 1352[0:Res:64.1,855.0] ordered(cons(u,v)) || -> ordered(snoc(v,m_Ldr(w)))*. % 156.72/156.95 1353[0:Res:82.1,855.0] ordered(cons(u,v)) || -> ordered(snoc(v,m_Ack(w,x)))*. % 156.72/156.95 1379[0:Res:7.0,65.0] || -> leq(host(u),s(nbr_proc))*. % 156.72/156.95 1494[0:NCh:97.2,97.0,83.1,26.0] || leq(u,v)*+ equal(s(v),u)* -> . % 156.72/156.95 1837[0:Res:1379.0,96.0] || leq(s(nbr_proc),host(u))* -> equal(s(nbr_proc),host(u)). % 156.72/156.95 1980[0:Res:48.0,102.0] || -> leq(s(u),v)* leq(v,u)* equal(v,s(u)). % 156.72/156.95 2071[0:MRR:1980.2,62.0] || -> leq(s(u),v)* leq(v,u)*. % 156.72/156.95 2409[1:Spt:1166.1] || -> equal(skc8,q_nil)**. % 156.72/156.95 2410[1:Rew:2409.0,63.0] || -> equal(cons(m_Halt(skc7),q_nil),queue(host(skc6)))**. % 156.72/156.95 2449[1:Rew:56.0,2410.0] || -> equal(snoc(q_nil,m_Halt(skc7)),queue(host(skc6)))**. % 156.72/156.95 2481[1:SpR:2449.0,95.0] || -> equal(snoc(cons(u,q_nil),m_Halt(skc7)),cons(u,queue(host(skc6))))**. % 156.72/156.95 2490[1:Rew:56.0,2481.0] || -> equal(snoc(snoc(q_nil,u),m_Halt(skc7)),cons(u,queue(host(skc6))))**. % 156.72/156.95 3136[0:EqR:1035.1] pidElem(m_NotNorm(u)) || -> equal(m_Down(skf5(m_NotNorm(u))),m_NotNorm(u))**. % 156.72/156.95 3139[0:MRR:3136.1,35.0] pidElem(m_NotNorm(u)) || -> . % 156.72/156.95 3369[0:SoR:847.0,17.0] || -> pidElem(u) ordered(snoc(cons(u,q_nil),v))*. % 156.72/156.95 3370[0:Rew:56.0,3369.1] || -> pidElem(u) ordered(snoc(snoc(q_nil,u),v))*. % 156.72/156.95 3375[1:SpR:2490.0,3370.1] || -> pidElem(u) ordered(cons(u,queue(host(skc6))))*. % 156.72/156.95 3386[1:SoR:1353.0,3375.1] || -> ordered(snoc(queue(host(skc6)),m_Ack(u,v)))* pidElem(w)*. % 156.72/156.95 3388[1:SoR:1352.0,3375.1] || -> ordered(snoc(queue(host(skc6)),m_Ldr(u)))* pidElem(v)*. % 159.91/160.17 3414[2:Spt:3388.1] || -> pidElem(u)*. % 159.91/160.17 3415[2:UnC:3414.0,3139.0] || -> . % 159.91/160.17 3416[2:Spt:3415.0,3388.0] || -> ordered(snoc(queue(host(skc6)),m_Ldr(u)))*. % 159.91/160.17 3427[3:Spt:3386.1] || -> pidElem(u)*. % 159.91/160.17 3428[3:UnC:3427.0,3139.0] || -> . % 159.91/160.17 3429[3:Spt:3428.0,3386.0] || -> ordered(snoc(queue(host(skc6)),m_Ack(u,v)))*. % 159.91/160.17 3451[0:Res:358.0,840.0] || -> equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6))** setIn(skc11,pids). % 159.91/160.17 3455[4:Spt:3451.0] || -> equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6))**. % 159.91/160.17 3471[4:SpL:3455.0,93.0] || equal(m_Ack(skc7,skc6),m_Ack(u,v))* -> equal(skc10,u). % 159.91/160.17 3472[4:SpL:3455.0,94.0] || equal(m_Ack(skc7,skc6),m_Ack(u,v))* -> equal(skc11,v). % 159.91/160.17 3493[4:EqR:3471.0] || -> equal(skc10,skc7)**. % 159.91/160.17 3526[4:Rew:3493.0,486.1] || setIn(u,alive) elem(m_Halt(skc7),queue(host(v)))* equal(index(status__dfg,host(u)),norm) equal(index(ldr,host(u)),host(u))**+ -> leq(nbr_proc,host(u)). % 159.91/160.17 3697[4:EqR:3472.0] || -> equal(skc11,skc6)**. % 159.91/160.17 3699[4:Rew:3697.0,452.0] || -> equal(host(skc6),nbr_proc)**. % 159.91/160.17 3737[4:Rew:3699.0,2449.0] || -> equal(snoc(q_nil,m_Halt(skc7)),queue(nbr_proc))**. % 159.91/160.17 3790[4:Rew:3699.0,286.0] || leq(host(skc9),nbr_proc)*l leq(host(skc6),host(skc9)) -> . % 159.91/160.17 3841[4:Rew:3699.0,3790.1] || leq(host(skc9),nbr_proc)*l leq(nbr_proc,host(skc9)) -> . % 159.91/160.17 3842[4:MRR:3841.0,7.0] || leq(nbr_proc,host(skc9))*r -> . % 159.91/160.17 4630[0:EqR:1171.0] || -> equal(last(cons(u,v)),u) elem(last(cons(u,v)),v)*. % 159.91/160.17 4654[0:SpR:95.0,4630.1] || -> equal(last(cons(u,snoc(v,w))),u) elem(last(snoc(cons(u,v),w)),snoc(v,w))*. % 159.91/160.17 4670[0:Rew:44.0,4654.1,44.0,4654.0,95.0,4654.0] || -> equal(u,v)* elem(u,snoc(w,u))*. % 159.91/160.17 5740[4:SpR:3737.0,4670.1] || -> equal(m_Halt(skc7),u)* elem(m_Halt(skc7),queue(nbr_proc))*. % 159.91/160.17 6321[4:AED:8.0,5740.0] || -> elem(m_Halt(skc7),queue(nbr_proc))*. % 159.91/160.17 6933[0:Res:7.0,1494.0] || equal(s(nbr_proc),host(u))* -> . % 159.91/160.17 7060[0:MRR:1837.1,6933.0] || leq(s(nbr_proc),host(u))* -> . % 159.91/160.17 8427[0:NCh:97.2,97.0,2071.0,7060.0] || equal(u,host(v))* -> leq(u,nbr_proc). % 159.91/160.17 49922[4:SpL:50.0,3526.3] || setIn(skc9,alive) elem(m_Halt(skc7),queue(host(u)))* equal(index(status__dfg,host(skc9)),norm) equal(host(skc9),host(skc9)) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 49923[4:Obv:49922.3] || setIn(skc9,alive) elem(m_Halt(skc7),queue(host(u)))* equal(index(status__dfg,host(skc9)),norm) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 49924[4:Rew:31.0,49923.2] || setIn(skc9,alive) elem(m_Halt(skc7),queue(host(u)))* equal(norm,norm) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 49925[4:Obv:49924.2] || setIn(skc9,alive) elem(m_Halt(skc7),queue(host(u)))* -> leq(nbr_proc,host(skc9)). % 159.91/160.17 49926[4:MRR:49925.0,49925.2,3.0,3842.0] || elem(m_Halt(skc7),queue(host(u)))* -> . % 159.91/160.17 49929[4:SpL:3699.0,49926.0] || elem(m_Halt(skc7),queue(nbr_proc))* -> . % 159.91/160.17 49936[4:MRR:49929.0,6321.0] || -> . % 159.91/160.17 49939[4:Spt:49936.0,3451.0,3455.0] || equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6))** -> . % 159.91/160.17 49940[4:Spt:49936.0,3451.1] || -> setIn(skc11,pids)*. % 159.91/160.17 49955[4:MRR:358.1,49939.0] || -> elem(m_Ack(skc10,skc11),queue(host(skc7)))*. % 159.91/160.17 54676[0:NCh:97.2,97.0,286.0,7.0] || equal(host(skc6),nbr_proc) leq(host(skc6),host(skc9))*r -> . % 159.91/160.17 55734[0:SpL:21.0,493.3] || setIn(skc10,alive) leq(nbr_proc,index(pendack,host(skc10))) equal(host(u),index(pendack,host(skc10))) elem(m_Ack(skc10,u),queue(host(skc7)))* equal(index(status__dfg,host(skc10)),elec_2) -> . % 159.91/160.17 55741[0:Rew:127.0,55734.4,21.0,55734.4,453.0,55734.2,21.0,55734.2,453.0,55734.1,21.0,55734.1] || setIn(skc10,alive) leq(nbr_proc,nbr_proc) equal(host(u),nbr_proc) elem(m_Ack(skc10,u),queue(host(skc7)))* equal(elec_2,elec_2) -> . % 159.91/160.17 55742[0:Obv:55741.4] || setIn(skc10,alive) leq(nbr_proc,nbr_proc) equal(host(u),nbr_proc) elem(m_Ack(skc10,u),queue(host(skc7)))* -> . % 159.91/160.17 55743[0:MRR:55742.0,55742.1,2.0,8427.1] || equal(host(u),nbr_proc) elem(m_Ack(skc10,u),queue(host(skc7)))* -> . % 159.91/160.17 68966[4:Res:49955.0,55743.1] || equal(host(skc11),nbr_proc)** -> . % 159.91/160.17 68967[4:Rew:452.0,68966.0] || equal(nbr_proc,nbr_proc)* -> . % 159.91/160.17 68968[4:Obv:68967.0] || -> . % 159.91/160.17 68971[1:Spt:68968.0,1166.1,2409.0] || equal(skc8,q_nil)** -> . % 159.91/160.17 68972[1:Spt:68968.0,1166.0,1166.2] || equal(m_Ack(skc6,u),last(skc8))** -> setIn(skc6,pids). % 159.91/160.17 70200[2:Spt:358.1] || -> equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6))**. % 159.91/160.17 70226[2:SpL:70200.0,93.0] || equal(m_Ack(skc7,skc6),m_Ack(u,v))* -> equal(skc10,u). % 159.91/160.17 70227[2:SpL:70200.0,94.0] || equal(m_Ack(skc7,skc6),m_Ack(u,v))* -> equal(skc11,v). % 159.91/160.17 70430[0:SpL:50.0,486.3] || setIn(skc9,alive) elem(m_Halt(skc10),queue(host(u)))* equal(index(status__dfg,host(skc9)),norm) equal(host(skc9),host(skc9)) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 70432[0:Obv:70430.3] || setIn(skc9,alive) elem(m_Halt(skc10),queue(host(u)))* equal(index(status__dfg,host(skc9)),norm) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 70433[0:Rew:31.0,70432.2] || setIn(skc9,alive) elem(m_Halt(skc10),queue(host(u)))* equal(norm,norm) -> leq(nbr_proc,host(skc9)). % 159.91/160.17 70434[0:Obv:70433.2] || setIn(skc9,alive) elem(m_Halt(skc10),queue(host(u)))* -> leq(nbr_proc,host(skc9)). % 159.91/160.17 70435[0:MRR:70434.0,3.0] || elem(m_Halt(skc10),queue(host(u)))* -> leq(nbr_proc,host(skc9)). % 159.91/160.17 75874[2:EqR:70226.0] || -> equal(skc10,skc7)**. % 159.91/160.17 77165[2:Rew:75874.0,70435.0] || elem(m_Halt(skc7),queue(host(u)))* -> leq(nbr_proc,host(skc9)). % 159.91/160.17 78437[2:EqR:70227.0] || -> equal(skc11,skc6)**. % 159.91/160.17 78441[2:Rew:78437.0,452.0] || -> equal(host(skc6),nbr_proc)**. % 159.91/160.17 78525[2:Rew:78441.0,536.0] || equal(queue(nbr_proc),q_nil)** -> . % 159.91/160.17 78526[2:Rew:78441.0,534.0] || -> equal(head(queue(nbr_proc)),m_Halt(skc7))**. % 159.91/160.17 78953[2:Rew:78441.0,54676.1,78441.0,54676.0] || equal(nbr_proc,nbr_proc) leq(nbr_proc,host(skc9))*r -> . % 159.91/160.17 78954[2:Obv:78953.0] || leq(nbr_proc,host(skc9))*r -> . % 159.91/160.17 78955[2:MRR:77165.1,78954.0] || elem(m_Halt(skc7),queue(host(u)))* -> . % 159.91/160.17 80082[2:SpL:78441.0,78955.0] || elem(m_Halt(skc7),queue(nbr_proc))* -> . % 159.91/160.17 80105[2:Res:780.2,80082.0] || equal(head(queue(nbr_proc)),m_Halt(skc7))** -> equal(queue(nbr_proc),q_nil). % 159.91/160.17 80109[2:Rew:78526.0,80105.0] || equal(m_Halt(skc7),m_Halt(skc7))* -> equal(queue(nbr_proc),q_nil). % 159.91/160.17 80110[2:Obv:80109.0] || -> equal(queue(nbr_proc),q_nil)**. % 159.91/160.17 80111[2:MRR:80110.0,78525.0] || -> . % 159.91/160.17 80114[2:Spt:80111.0,358.1,70200.0] || equal(m_Ack(skc10,skc11),m_Ack(skc7,skc6))** -> . % 159.91/160.17 80115[2:Spt:80111.0,358.0] || -> elem(m_Ack(skc10,skc11),queue(host(skc7)))*. % 159.91/160.17 91947[2:Res:80115.0,55743.1] || equal(host(skc11),nbr_proc)** -> . % 159.91/160.17 91948[2:Rew:452.0,91947.0] || equal(nbr_proc,nbr_proc)* -> . % 159.91/160.17 91949[2:Obv:91948.0] || -> . % 159.91/160.17 % SZS output end Refutation % 159.91/160.17 Formulae used in the proof : conj axiom_04 axiom_05 axiom_52 axiom_58 axiom_16 axiom_19 axiom_35 axiom_37 axiom_41 axiom_60 axiom_43 axiom_53 axiom_50 axiom_48 axiom_61 axiom_56 axiom_64 axiom_46 axiom_47 axiom_55 axiom_63 axiom_39 axiom_40 axiom axiom_31 axiom_32 axiom_44 axiom_62 % 159.91/160.17 %------------------------------------------------------------------------------