%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV450+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:08 EDT 2022 % Result : Timeout 288.13s 288.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV450+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 18:27:33 EDT 2022 % 0.13/0.35 % CPUTime : % 288.13/288.31 % 288.13/288.31 SPASS V 3.9 % 288.13/288.31 SPASS beiseite: Proof found. % 288.13/288.31 % SZS status Theorem % 288.13/288.31 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 288.13/288.31 SPASS derived 77552 clauses, backtracked 6973 clauses, performed 24 splits and kept 36695 clauses. % 288.13/288.31 SPASS allocated 151538 KBytes. % 288.13/288.31 SPASS spent 0:4:46.22 on the problem. % 288.13/288.31 0:00:00.04 for the input. % 288.13/288.31 0:00:00.05 for the FLOTTER CNF translation. % 288.13/288.31 0:00:01.09 for inferences. % 288.13/288.31 0:00:03.93 for the backtracking. % 288.13/288.31 0:4:40.10 for the reduction. % 288.13/288.31 % 288.13/288.31 % 288.13/288.31 Here is a proof with depth 4, length 62 : % 288.13/288.31 % SZS output start Refutation % 288.13/288.31 3[0:Inp] || -> setIn(skc13,alive)*. % 288.13/288.31 4[0:Inp] || -> setIn(skc8,alive)*. % 288.13/288.31 6[0:Inp] || -> elem(m_Down(skc14),skc10)*. % 288.13/288.31 8[0:Inp] || -> leq(host(u),nbr_proc)*l. % 288.13/288.31 22[0:Inp] || -> equal(host(skc15),host(skc12))**. % 288.13/288.31 23[0:Inp] || -> equal(host(skc14),host(skc13))**. % 288.13/288.31 24[0:Inp] || -> equal(host(skc12),host(skc8))**. % 288.13/288.31 25[0:Inp] || -> equal(host(skc13),host(skc11))**. % 288.13/288.31 33[0:Inp] || equal(host(skc13),host(skc8))** -> . % 288.13/288.31 35[0:Inp] || -> leq(nbr_proc,index(pendack,host(skc8)))*r. % 288.13/288.31 38[0:Inp] || equal(m_Down(u),m_Ldr(v))* -> . % 288.13/288.31 53[0:Inp] || -> equal(index(pendack,host(skc8)),host(skc9))**. % 288.13/288.31 68[0:Inp] || -> elem(m_Down(skc15),snoc(queue(host(skc13)),m_Ldr(skc8)))*. % 288.13/288.31 80[0:Inp] || elem(u,v) -> elem(u,cons(w,v))*. % 288.13/288.31 97[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 288.13/288.31 99[0:Inp] || -> setIn(host(skc11),index(acks,host(skc8)))* equal(host(skc11),host(skc9)). % 288.13/288.31 100[0:Inp] || -> equal(cons(m_Ack(index(elid,host(skc8)),skc9),skc10),queue(host(skc8)))**. % 288.13/288.31 102[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 288.13/288.31 120[0:Inp] || setIn(u,alive) setIn(v,alive) equal(host(w),host(u))* equal(host(x),host(v))* elem(m_Down(x),queue(host(u)))*+ elem(m_Down(w),queue(host(v)))* -> equal(host(u),host(v))*. % 288.13/288.31 121[0:Rew:25.0,23.0] || -> equal(host(skc14),host(skc11))**. % 288.13/288.31 122[0:Rew:24.0,22.0] || -> equal(host(skc15),host(skc8))**. % 288.13/288.31 123[0:Rew:25.0,33.0] || equal(host(skc11),host(skc8))** -> . % 288.13/288.31 127[0:Rew:25.0,68.0] || -> elem(m_Down(skc15),snoc(queue(host(skc11)),m_Ldr(skc8)))*. % 288.13/288.31 128[0:Rew:53.0,35.0] || -> leq(nbr_proc,host(skc9))*r. % 288.13/288.31 140[0:Res:3.0,120.5] || setIn(u,alive) equal(host(v),host(u))* elem(m_Down(w),queue(host(u)))* elem(m_Down(v),queue(host(skc13)))* equal(host(w),host(skc13)) -> equal(host(skc13),host(u)). % 288.13/288.31 147[0:Res:6.0,80.0] || -> elem(m_Down(skc14),cons(u,skc10))*. % 288.13/288.31 330[0:Res:127.0,102.0] || -> equal(m_Ldr(skc8),m_Down(skc15)) elem(m_Down(skc15),queue(host(skc11)))*. % 288.13/288.31 334[0:Res:128.0,97.1] || leq(host(skc9),nbr_proc)*l -> equal(host(skc9),nbr_proc). % 288.13/288.31 404[0:MRR:334.0,8.0] || -> equal(host(skc9),nbr_proc)**. % 288.13/288.31 407[0:Rew:404.0,99.1] || -> equal(host(skc11),nbr_proc) setIn(host(skc11),index(acks,host(skc8)))*. % 288.13/288.31 434[0:Rew:25.0,140.5,25.0,140.4,25.0,140.3] || setIn(u,alive) equal(host(v),host(u))* equal(host(w),host(skc11)) elem(m_Down(w),queue(host(u)))*+ elem(m_Down(v),queue(host(skc11)))* -> equal(host(skc11),host(u)). % 288.13/288.31 436[1:Spt:407.0] || -> equal(host(skc11),nbr_proc)**. % 288.13/288.31 437[1:Rew:436.0,434.4] || setIn(u,alive) equal(host(v),host(u))* equal(host(w),host(skc11)) elem(m_Down(w),queue(host(u)))* elem(m_Down(v),queue(nbr_proc))* -> equal(host(skc11),host(u)). % 288.13/288.31 443[1:Rew:436.0,330.1] || -> equal(m_Ldr(skc8),m_Down(skc15)) elem(m_Down(skc15),queue(nbr_proc))*. % 288.13/288.31 449[1:Rew:436.0,121.0] || -> equal(host(skc14),nbr_proc)**. % 288.13/288.31 450[1:Rew:436.0,123.0] || equal(host(skc8),nbr_proc)** -> . % 288.13/288.31 457[1:Rew:436.0,437.5,436.0,437.2] || setIn(u,alive) equal(host(v),host(u))* equal(host(w),nbr_proc) elem(m_Down(w),queue(host(u)))*+ elem(m_Down(v),queue(nbr_proc))* -> equal(host(u),nbr_proc). % 288.13/288.31 713[2:Spt:443.0] || -> equal(m_Ldr(skc8),m_Down(skc15))**. % 288.13/288.31 714[2:UnC:713.0,38.0] || -> . % 288.13/288.31 715[2:Spt:714.0,443.0,713.0] || equal(m_Ldr(skc8),m_Down(skc15))** -> . % 288.13/288.31 716[2:Spt:714.0,443.1] || -> elem(m_Down(skc15),queue(nbr_proc))*. % 288.13/288.31 852[0:SpR:100.0,147.0] || -> elem(m_Down(skc14),queue(host(skc8)))*. % 288.13/288.31 34470[1:Res:852.0,457.3] || setIn(skc8,alive) equal(host(u),host(skc8)) equal(host(skc14),nbr_proc) elem(m_Down(u),queue(nbr_proc))* -> equal(host(skc8),nbr_proc). % 288.13/288.31 34477[1:Rew:449.0,34470.2] || setIn(skc8,alive) equal(host(u),host(skc8)) equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc))* -> equal(host(skc8),nbr_proc). % 288.13/288.31 34478[1:Obv:34477.2] || setIn(skc8,alive) equal(host(u),host(skc8)) elem(m_Down(u),queue(nbr_proc))* -> equal(host(skc8),nbr_proc). % 288.13/288.31 34479[1:MRR:34478.0,34478.3,4.0,450.0] || equal(host(u),host(skc8)) elem(m_Down(u),queue(nbr_proc))* -> . % 288.13/288.31 34485[2:Res:716.0,34479.1] || equal(host(skc15),host(skc8))** -> . % 288.13/288.31 34489[2:Rew:122.0,34485.0] || equal(host(skc8),host(skc8))* -> . % 288.13/288.31 34490[2:Obv:34489.0] || -> . % 288.13/288.31 34491[1:Spt:34490.0,407.0,436.0] || equal(host(skc11),nbr_proc)** -> . % 288.13/288.31 34492[1:Spt:34490.0,407.1] || -> setIn(host(skc11),index(acks,host(skc8)))*. % 288.13/288.31 34770[2:Spt:330.0] || -> equal(m_Ldr(skc8),m_Down(skc15))**. % 288.13/288.31 34771[2:UnC:34770.0,38.0] || -> . % 288.13/288.31 34772[2:Spt:34771.0,330.0,34770.0] || equal(m_Ldr(skc8),m_Down(skc15))** -> . % 288.13/288.31 34773[2:Spt:34771.0,330.1] || -> elem(m_Down(skc15),queue(host(skc11)))*. % 288.13/288.31 37539[0:Res:852.0,434.3] || setIn(skc8,alive) equal(host(u),host(skc8)) equal(host(skc14),host(skc11)) elem(m_Down(u),queue(host(skc11)))* -> equal(host(skc11),host(skc8)). % 288.13/288.31 37549[0:Rew:121.0,37539.2] || setIn(skc8,alive) equal(host(u),host(skc8)) equal(host(skc11),host(skc11)) elem(m_Down(u),queue(host(skc11)))* -> equal(host(skc11),host(skc8)). % 288.13/288.31 37550[0:Obv:37549.2] || setIn(skc8,alive) equal(host(u),host(skc8)) elem(m_Down(u),queue(host(skc11)))* -> equal(host(skc11),host(skc8)). % 288.13/288.31 37551[0:MRR:37550.0,37550.3,4.0,123.0] || equal(host(u),host(skc8)) elem(m_Down(u),queue(host(skc11)))* -> . % 288.13/288.31 88108[2:Res:34773.0,37551.1] || equal(host(skc15),host(skc8))** -> . % 288.13/288.31 88112[2:Rew:122.0,88108.0] || equal(host(skc8),host(skc8))* -> . % 288.13/288.31 88113[2:Obv:88112.0] || -> . % 288.13/288.31 % SZS output end Refutation % 288.13/288.31 Formulae used in the proof : conj axiom_04 axiom_18 axiom_46 axiom_61 axiom_47 % 288.13/288.31 %------------------------------------------------------------------------------