%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV473+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:13 EDT 2022 % Result : Theorem 40.78s 40.97s % Output : Refutation 40.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV473+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n008.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 : Tue Jun 14 22:52:52 EDT 2022 % 0.12/0.34 % CPUTime : % 40.78/40.97 % 40.78/40.97 SPASS V 3.9 % 40.78/40.97 SPASS beiseite: Proof found. % 40.78/40.97 % SZS status Theorem % 40.78/40.97 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.78/40.97 SPASS derived 39222 clauses, backtracked 846 clauses, performed 36 splits and kept 13161 clauses. % 40.78/40.97 SPASS allocated 126351 KBytes. % 40.78/40.97 SPASS spent 0:0:40.26 on the problem. % 40.78/40.97 0:00:00.03 for the input. % 40.78/40.97 0:00:00.05 for the FLOTTER CNF translation. % 40.78/40.97 0:00:00.54 for inferences. % 40.78/40.97 0:00:00.84 for the backtracking. % 40.78/40.97 0:0:38.49 for the reduction. % 40.78/40.97 % 40.78/40.97 % 40.78/40.97 Here is a proof with depth 3, length 62 : % 40.78/40.97 % SZS output start Refutation % 40.78/40.97 2[0:Inp] || -> setIn(skc12,alive)*. % 40.78/40.97 5[0:Inp] || -> elem(m_Down(skc14),skc11)*. % 40.78/40.97 6[0:Inp] || -> equal(host(skc13),nbr_proc)**. % 40.78/40.97 8[0:Inp] || -> leq(host(u),nbr_proc)*l. % 40.78/40.97 22[0:Inp] || -> equal(host(skc15),host(skc13))**. % 40.78/40.97 23[0:Inp] || -> equal(host(skc13),host(skc8))**. % 40.78/40.97 30[0:Inp] || -> equal(index(status__dfg,host(skc13)),elec_1)**. % 40.78/40.97 31[0:Inp] || -> elem(m_Down(skc15),queue(host(skc12)))*. % 40.78/40.97 48[0:Inp] || -> leq(u,v)* leq(v,u)*. % 40.78/40.97 49[0:Inp] || leq(host(u),skf5(v,u))*r -> . % 40.78/40.97 61[0:Inp] || equal(u,v)* -> leq(v,u). % 40.78/40.97 64[0:Inp] || -> equal(cons(m_Ack(skc10,skc9),skc11),queue(host(skc8)))**. % 40.78/40.97 76[0:Inp] || elem(u,v) -> elem(u,cons(w,v))*. % 40.78/40.97 92[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 40.78/40.97 93[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 40.78/40.97 111[0:Inp] || leq(s(zero),u) -> leq(host(skc13),u) setIn(u,index(down,host(skc13)))* equal(u,host(skc14)). % 40.78/40.97 120[0:Inp] || elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(w,alive) elem(m_Down(x),queue(host(w)))* equal(host(v),host(x))* -> leq(s(zero),skf5(u,v)). % 40.78/40.97 121[0:Inp] || equal(skf5(u,v),host(u)) elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(w,alive) elem(m_Down(x),queue(host(w)))* equal(host(v),host(x))* -> . % 40.78/40.97 122[0:Inp] || setIn(skf5(u,v),index(down,host(v)))* elem(m_Down(u),queue(host(v))) equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(w,alive) elem(m_Down(x),queue(host(w)))* equal(host(v),host(x))* -> . % 40.78/40.97 123[0:Rew:6.0,23.0] || -> equal(host(skc8),nbr_proc)**. % 40.78/40.97 124[0:Rew:6.0,22.0] || -> equal(host(skc15),nbr_proc)**. % 40.78/40.97 125[0:Rew:6.0,30.0] || -> equal(index(status__dfg,nbr_proc),elec_1)**. % 40.78/40.97 128[0:Rew:123.0,64.0] || -> equal(cons(m_Ack(skc10,skc9),skc11),queue(nbr_proc))**. % 40.78/40.97 130[0:Rew:6.0,111.2,6.0,111.1] || leq(s(zero),u) -> equal(u,host(skc14)) setIn(u,index(down,nbr_proc))* leq(nbr_proc,u). % 40.78/40.97 177[0:Res:5.0,76.0] || -> elem(m_Down(skc14),cons(u,skc11))*. % 40.78/40.97 274[0:Res:31.0,120.4] || elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),host(skc15)) -> leq(s(zero),skf5(u,v)). % 40.78/40.97 275[0:Res:31.0,122.5] || setIn(skf5(u,v),index(down,host(v)))* elem(m_Down(u),queue(host(v))) equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),host(skc15)) -> . % 40.78/40.97 276[0:Res:31.0,121.5] || equal(skf5(u,v),host(u)) elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),host(skc15)) -> . % 40.78/40.97 296[0:Res:48.1,49.0] || -> leq(skf5(u,v),host(v))*l. % 40.78/40.97 297[0:Res:61.1,49.0] || equal(skf5(u,v),host(v))** -> . % 40.78/40.97 429[0:Rew:124.0,276.5] || equal(skf5(u,v),host(u)) elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),nbr_proc) -> . % 40.78/40.97 430[0:Obv:429.3] || equal(skf5(u,v),host(u)) elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) setIn(skc12,alive) equal(host(v),nbr_proc) -> . % 40.78/40.97 431[0:MRR:430.3,2.0] || equal(host(u),nbr_proc) elem(m_Down(v),queue(host(u)))* equal(skf5(v,u),host(v)) equal(index(status__dfg,host(u)),elec_1) -> . % 40.78/40.97 434[0:Rew:124.0,275.5] || setIn(skf5(u,v),index(down,host(v)))* elem(m_Down(u),queue(host(v))) equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),nbr_proc) -> . % 40.78/40.97 435[0:Obv:434.3] || setIn(skf5(u,v),index(down,host(v)))* elem(m_Down(u),queue(host(v))) equal(index(status__dfg,host(v)),elec_1) setIn(skc12,alive) equal(host(v),nbr_proc) -> . % 40.78/40.97 436[0:MRR:435.3,2.0] || equal(host(u),nbr_proc) elem(m_Down(v),queue(host(u))) setIn(skf5(v,u),index(down,host(u)))* equal(index(status__dfg,host(u)),elec_1) -> . % 40.78/40.97 443[0:Rew:124.0,274.4] || elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc12,alive) equal(host(v),nbr_proc) -> leq(s(zero),skf5(u,v)). % 40.78/40.97 444[0:Obv:443.2] || elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) setIn(skc12,alive) equal(host(v),nbr_proc) -> leq(s(zero),skf5(u,v)). % 40.78/40.97 445[0:MRR:444.2,2.0] || equal(host(u),nbr_proc) elem(m_Down(v),queue(host(u)))* equal(index(status__dfg,host(u)),elec_1) -> leq(s(zero),skf5(v,u)). % 40.78/40.97 494[0:SpR:128.0,177.0] || -> elem(m_Down(skc14),queue(nbr_proc))*. % 40.78/40.97 1185[0:NCh:93.2,93.1,48.1,49.0] || leq(host(u),v)*+ -> leq(skf5(w,u),v)*. % 40.78/40.97 1661[0:NCh:93.2,93.0,92.0,8.0] || equal(nbr_proc,u) leq(u,host(v))* -> equal(u,host(v)). % 40.78/40.97 5602[0:Res:296.0,1661.1] || equal(skf5(u,v),nbr_proc)** -> equal(skf5(u,v),host(v)). % 40.78/40.97 5674[0:MRR:5602.1,297.0] || equal(skf5(u,v),nbr_proc)** -> . % 40.78/40.97 7297[0:Res:8.0,1185.0] || -> leq(skf5(u,v),nbr_proc)*l. % 40.78/40.97 7872[0:Res:7297.0,92.0] || leq(nbr_proc,skf5(u,v))*r -> equal(skf5(u,v),nbr_proc). % 40.78/40.97 7899[0:MRR:7872.1,5674.0] || leq(nbr_proc,skf5(u,v))*r -> . % 40.78/40.97 15781[0:SpL:123.0,431.1] || equal(host(skc8),nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc8),host(u)) equal(index(status__dfg,host(skc8)),elec_1) -> . % 40.78/40.97 15794[0:Rew:125.0,15781.3,123.0,15781.3,123.0,15781.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc8),host(u)) equal(elec_1,elec_1) -> . % 40.78/40.97 15795[0:Obv:15794.3] || elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc8),host(u)) -> . % 40.78/40.97 18230[0:SpL:123.0,436.2] || equal(host(skc8),nbr_proc) elem(m_Down(u),queue(host(skc8))) setIn(skf5(u,skc8),index(down,nbr_proc))* equal(index(status__dfg,host(skc8)),elec_1) -> . % 40.78/40.97 18236[0:Rew:125.0,18230.3,123.0,18230.3,123.0,18230.1,123.0,18230.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc)) setIn(skf5(u,skc8),index(down,nbr_proc))* equal(elec_1,elec_1) -> . % 40.78/40.97 18237[0:Obv:18236.3] || elem(m_Down(u),queue(nbr_proc)) setIn(skf5(u,skc8),index(down,nbr_proc))* -> . % 40.78/40.97 41367[0:SpL:123.0,445.1] || equal(host(skc8),nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(index(status__dfg,host(skc8)),elec_1) -> leq(s(zero),skf5(u,skc8)). % 40.78/40.97 41380[0:Rew:125.0,41367.2,123.0,41367.2,123.0,41367.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(elec_1,elec_1) -> leq(s(zero),skf5(u,skc8)). % 40.78/40.97 41381[0:Obv:41380.2] || elem(m_Down(u),queue(nbr_proc))* -> leq(s(zero),skf5(u,skc8)). % 40.78/40.97 45205[0:Res:130.2,18237.1] || leq(s(zero),skf5(u,skc8)) elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc8),host(skc14)) leq(nbr_proc,skf5(u,skc8)). % 40.78/40.97 45206[0:MRR:45205.3,7899.0] || leq(s(zero),skf5(u,skc8)) elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc8),host(skc14)). % 40.78/40.97 45207[0:MRR:45206.0,41381.1] || elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc8),host(skc14)). % 40.78/40.97 45208[0:Rew:45207.1,15795.1] || elem(m_Down(u),queue(nbr_proc))* equal(host(skc14),host(u)) -> . % 40.78/40.97 45254[0:Res:494.0,45208.0] || equal(host(skc14),host(skc14))* -> . % 40.78/40.97 45259[0:Obv:45254.0] || -> . % 40.78/40.97 % SZS output end Refutation % 40.78/40.97 Formulae used in the proof : conj axiom_02 axiom_62 axiom_63 axiom_58 axiom_04 axiom_60 axiom_61 axiom_46 % 40.78/40.97 %------------------------------------------------------------------------------