%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV479+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:14 EDT 2022 % Result : Theorem 10.49s 10.71s % Output : Refutation 10.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SWV479+1 : TPTP v8.1.0. Released v4.0.0. % 0.13/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n028.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Wed Jun 15 12:46:25 EDT 2022 % 0.14/0.36 % CPUTime : % 10.49/10.71 % 10.49/10.71 SPASS V 3.9 % 10.49/10.71 SPASS beiseite: Proof found. % 10.49/10.71 % SZS status Theorem % 10.49/10.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.49/10.71 SPASS derived 19019 clauses, backtracked 2 clauses, performed 7 splits and kept 6558 clauses. % 10.49/10.71 SPASS allocated 111519 KBytes. % 10.49/10.71 SPASS spent 0:0:10.22 on the problem. % 10.49/10.71 0:00:00.04 for the input. % 10.49/10.71 0:00:00.07 for the FLOTTER CNF translation. % 10.49/10.71 0:00:00.24 for inferences. % 10.49/10.71 0:00:00.02 for the backtracking. % 10.49/10.71 0:00:09.73 for the reduction. % 10.49/10.71 % 10.49/10.71 % 10.49/10.71 Here is a proof with depth 3, length 61 : % 10.49/10.71 % SZS output start Refutation % 10.49/10.71 2[0:Inp] || -> setIn(skc8,alive)*. % 10.49/10.71 3[0:Inp] || -> setIn(skc13,alive)*. % 10.49/10.71 7[0:Inp] || -> leq(host(u),nbr_proc)*l. % 10.49/10.71 22[0:Inp] || -> leq(host(skc8),host(skc9))*r. % 10.49/10.71 23[0:Inp] || -> leq(nbr_proc,s(host(skc13)))*r. % 10.49/10.71 24[0:Inp] || -> leq(s(zero),host(u))*r. % 10.49/10.71 28[0:Inp] || leq(s(u),u)*l -> . % 10.49/10.71 30[0:Inp] || -> elem(m_Down(skc14),queue(host(skc13)))*. % 10.49/10.71 31[0:Inp] || -> equal(index(status__dfg,host(skc8)),elec_2)**. % 10.49/10.71 32[0:Inp] || -> leq(nbr_proc,index(pendack,host(skc8)))*r. % 10.49/10.71 34[0:Inp] || equal(host(skc13),host(skc8))** -> . % 10.49/10.71 36[0:Inp] || -> equal(s(host(skc13)),host(skc15))**. % 10.49/10.71 53[0:Inp] || -> leq(u,v)* leq(v,u)*. % 10.49/10.71 57[0:Inp] || -> equal(index(pendack,host(skc8)),host(skc9))**. % 10.49/10.71 69[0:Inp] || equal(u,v)* -> leq(v,u). % 10.49/10.71 70[0:Inp] || -> equal(cons(m_Down(skc9),skc10),queue(host(skc8)))**. % 10.49/10.71 83[0:Inp] || equal(u,v) -> elem(u,cons(v,w))*. % 10.49/10.71 100[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 10.49/10.71 101[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 10.49/10.71 106[0:Inp] || leq(u,s(v))* -> leq(u,v) equal(u,s(v)). % 10.49/10.71 107[0:Inp] || equal(host(u),host(v)) elem(m_Down(u),queue(host(v)))* -> . % 10.49/10.71 118[0:Inp] || leq(s(zero),u) -> equal(u,host(skc14)) setIn(u,index(down,host(skc13)))* leq(host(skc13),u). % 10.49/10.71 122[0:Inp] || setIn(u,alive) setIn(v,alive) setIn(host(u),index(down,host(v)))* equal(index(status__dfg,host(u)),elec_2) -> leq(index(pendack,host(u)),host(v)). % 10.49/10.71 124[0:Inp] || setIn(u,alive) setIn(v,alive) equal(host(u),host(w))* elem(m_Down(w),queue(host(v)))*+ equal(index(status__dfg,host(u)),elec_2) -> leq(index(pendack,host(u)),host(v))*. % 10.49/10.71 138[0:Rew:36.0,23.0] || -> leq(nbr_proc,host(skc15))*r. % 10.49/10.71 139[0:Rew:57.0,32.0] || -> leq(nbr_proc,host(skc9))*r. % 10.49/10.71 198[0:Res:2.0,122.3] || setIn(u,alive) setIn(host(skc8),index(down,host(u)))* equal(index(status__dfg,host(skc8)),elec_2) -> leq(index(pendack,host(skc8)),host(u)). % 10.49/10.71 214[0:Res:2.0,124.3] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc8),host(v)) equal(index(status__dfg,host(skc8)),elec_2) -> leq(index(pendack,host(skc8)),host(u)). % 10.49/10.71 323[0:Res:100.2,34.0] || leq(host(skc13),host(skc8))*l leq(host(skc8),host(skc13)) -> . % 10.49/10.71 365[0:Rew:57.0,198.3,31.0,198.2] || setIn(u,alive) setIn(host(skc8),index(down,host(u)))* equal(elec_2,elec_2) -> leq(host(skc9),host(u)). % 10.49/10.71 366[0:Obv:365.2] || setIn(u,alive) setIn(host(skc8),index(down,host(u)))* -> leq(host(skc9),host(u)). % 10.49/10.71 396[0:Rew:57.0,214.4,31.0,214.3] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc8),host(v)) equal(elec_2,elec_2) -> leq(host(skc9),host(u)). % 10.49/10.71 397[0:Obv:396.3] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc8),host(v)) -> leq(host(skc9),host(u)). % 10.49/10.71 685[0:SpR:70.0,83.1] || equal(u,m_Down(skc9)) -> elem(u,queue(host(skc8)))*. % 10.49/10.71 695[0:SpL:36.0,28.0] || leq(host(skc15),host(skc13))*l -> . % 10.49/10.71 746[0:NCh:101.2,101.0,695.0,7.0] || leq(nbr_proc,host(skc13))*r -> . % 10.49/10.71 1026[0:Res:685.1,107.1] || equal(m_Down(u),m_Down(skc9)) equal(host(u),host(skc8))* -> . % 10.49/10.71 1864[0:Res:138.0,100.0] || leq(host(skc15),nbr_proc)*l -> equal(host(skc15),nbr_proc). % 10.49/10.71 1865[0:Res:139.0,100.0] || leq(host(skc9),nbr_proc)*l -> equal(host(skc9),nbr_proc). % 10.49/10.71 1909[0:NCh:101.2,101.1,100.0,22.0] || equal(u,host(skc8)) leq(host(skc9),u)* -> equal(host(skc9),u). % 10.49/10.71 1950[0:MRR:1864.0,7.0] || -> equal(host(skc15),nbr_proc)**. % 10.49/10.71 1951[0:Rew:1950.0,36.0] || -> equal(s(host(skc13)),nbr_proc)**. % 10.49/10.71 2005[0:MRR:1865.0,7.0] || -> equal(host(skc9),nbr_proc)**. % 10.49/10.71 2012[0:Rew:2005.0,397.3] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc8),host(v)) -> leq(nbr_proc,host(u)). % 10.49/10.71 2013[0:Rew:2005.0,366.2] || setIn(u,alive) setIn(host(skc8),index(down,host(u)))* -> leq(nbr_proc,host(u)). % 10.49/10.71 2055[0:Rew:2005.0,1909.2,2005.0,1909.1] || equal(u,host(skc8))* leq(nbr_proc,u)*+ -> equal(nbr_proc,u). % 10.49/10.71 2115[0:SpL:2005.0,1026.1] || equal(m_Down(skc9),m_Down(skc9)) equal(host(skc8),nbr_proc)** -> . % 10.49/10.71 2118[0:Obv:2115.0] || equal(host(skc8),nbr_proc)** -> . % 10.49/10.71 2152[0:Res:53.0,106.0] || -> leq(s(u),v)* leq(v,u)* equal(v,s(u)). % 10.49/10.71 2200[0:MRR:2152.2,69.0] || -> leq(s(u),v)* leq(v,u)*. % 10.49/10.71 12020[0:Res:118.2,2013.1] || leq(s(zero),host(skc8)) setIn(skc13,alive)* -> equal(host(skc14),host(skc8)) leq(host(skc13),host(skc8)) leq(nbr_proc,host(skc13)). % 10.49/10.71 12025[0:MRR:12020.0,12020.1,12020.4,24.0,3.0,746.0] || -> equal(host(skc14),host(skc8))** leq(host(skc13),host(skc8)). % 10.49/10.71 21532[0:Res:30.0,2012.1] || setIn(skc13,alive)* equal(host(skc14),host(skc8)) -> leq(nbr_proc,host(skc13)). % 10.49/10.71 21538[0:MRR:21532.0,21532.2,3.0,746.0] || equal(host(skc14),host(skc8))** -> . % 10.49/10.71 21539[0:MRR:12025.0,21538.0] || -> leq(host(skc13),host(skc8))*l. % 10.49/10.71 21540[0:MRR:323.0,21539.0] || leq(host(skc8),host(skc13))*r -> . % 10.49/10.71 21697[0:NCh:101.2,101.1,21540.0,2200.1] || equal(host(skc8),u)* -> leq(s(host(skc13)),u)*. % 10.49/10.71 21718[0:Rew:1951.0,21697.1] || equal(host(skc8),u)* -> leq(nbr_proc,u). % 10.49/10.71 21719[0:MRR:2055.1,21718.1] || equal(u,host(skc8))* -> equal(nbr_proc,u). % 10.49/10.71 21724[0:EqR:21719.0] || -> equal(host(skc8),nbr_proc)**. % 10.49/10.71 21725[0:MRR:21724.0,2118.0] || -> . % 10.49/10.71 % SZS output end Refutation % 10.49/10.71 Formulae used in the proof : conj axiom_02 axiom_62 axiom_63 axiom_58 axiom_04 axiom_60 axiom_61 axiom_46 axiom_64 % 10.49/10.71 %------------------------------------------------------------------------------