%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV468+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:12 EDT 2022 % Result : Theorem 43.89s 44.07s % Output : Refutation 43.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV468+1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n005.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.33 % DateTime : Wed Jun 15 16:20:38 EDT 2022 % 0.13/0.33 % CPUTime : % 43.89/44.07 % 43.89/44.07 SPASS V 3.9 % 43.89/44.07 SPASS beiseite: Proof found. % 43.89/44.07 % SZS status Theorem % 43.89/44.07 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.89/44.07 SPASS derived 36977 clauses, backtracked 1396 clauses, performed 18 splits and kept 12732 clauses. % 43.89/44.07 SPASS allocated 125482 KBytes. % 43.89/44.07 SPASS spent 0:0:43.03 on the problem. % 43.89/44.07 0:00:00.03 for the input. % 43.89/44.07 0:00:00.05 for the FLOTTER CNF translation. % 43.89/44.07 0:00:00.46 for inferences. % 43.89/44.07 0:00:00.33 for the backtracking. % 43.89/44.07 0:0:41.94 for the reduction. % 43.89/44.07 % 43.89/44.07 % 43.89/44.07 Here is a proof with depth 8, length 59 : % 43.89/44.07 % SZS output start Refutation % 43.89/44.07 2[0:Inp] || -> setIn(skc6,alive)*. % 43.89/44.07 3[0:Inp] || -> setIn(skc11,alive)*. % 43.89/44.07 6[0:Inp] || -> leq(nbr_proc,host(skc6))*r. % 43.89/44.07 8[0:Inp] || -> leq(host(u),nbr_proc)*l. % 43.89/44.07 9[0:Inp] || equal(elec_1,elec_2)** -> . % 43.89/44.07 22[0:Inp] || -> equal(host(skc10),host(skc6))**. % 43.89/44.07 24[0:Inp] || -> leq(s(zero),host(u))*. % 43.89/44.07 29[0:Inp] || equal(host(skc11),host(skc6))** -> . % 43.89/44.07 32[0:Inp] || -> equal(index(status__dfg,host(skc11)),elec_2)**. % 43.89/44.07 43[0:Inp] || -> equal(head(cons(u,v)),u)**. % 43.89/44.07 48[0:Inp] || equal(snoc(u,v),q_nil)** -> . % 43.89/44.07 63[0:Inp] || -> equal(cons(m_Down(skc7),skc8),queue(host(skc6)))**. % 43.89/44.07 64[0:Inp] || leq(index(pendack,host(skc11)),host(skc10))*l -> . % 43.89/44.07 77[0:Inp] || equal(u,v) -> elem(u,cons(v,w))*. % 43.89/44.07 87[0:Inp] || -> equal(u,q_nil) equal(cons(head(u),tail(u)),u)**. % 43.89/44.07 93[0:Inp] || -> equal(cons(u,snoc(v,w)),snoc(cons(u,v),w))**. % 43.89/44.07 94[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 43.89/44.07 97[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 43.89/44.07 113[0:Inp] || leq(s(zero),u) -> equal(u,host(skc7)) setIn(u,index(down,host(skc6)))* leq(host(skc6),u). % 43.89/44.07 118[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)). % 43.89/44.07 122[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))*. % 43.89/44.07 132[0:Rew:22.0,64.0] || leq(index(pendack,host(skc11)),host(skc6))*l -> . % 43.89/44.07 258[0:Res:32.0,118.2] || setIn(u,alive) setIn(host(skc11),index(down,host(u)))* setIn(skc11,alive) -> leq(index(pendack,host(skc11)),host(u)). % 43.89/44.07 260[0:Res:32.0,122.4] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc11),host(v)) setIn(skc11,alive) -> leq(index(pendack,host(skc11)),host(u)). % 43.89/44.07 329[0:MRR:258.2,3.0] || setIn(u,alive) setIn(host(skc11),index(down,host(u)))* -> leq(index(pendack,host(skc11)),host(u)). % 43.89/44.07 352[0:MRR:260.3,3.0] || setIn(u,alive) elem(m_Down(v),queue(host(u)))* equal(host(skc11),host(v)) -> leq(index(pendack,host(skc11)),host(u)). % 43.89/44.07 635[0:SpR:87.1,77.1] || equal(u,head(v)) -> equal(v,q_nil) elem(u,v)*. % 43.89/44.07 663[0:SpR:93.0,43.0] || -> equal(head(snoc(cons(u,v),w)),u)**. % 43.89/44.07 679[0:SpR:63.0,663.0] || -> equal(head(snoc(queue(host(skc6)),u)),m_Down(skc7))**. % 43.89/44.07 797[0:Res:635.2,97.0] || equal(u,head(snoc(v,w)))* -> equal(snoc(v,w),q_nil) elem(u,v)* equal(u,w). % 43.89/44.07 805[0:MRR:797.1,48.0] || equal(u,head(snoc(v,w)))*+ -> elem(u,v)* equal(u,w). % 43.89/44.07 1709[0:Res:6.0,94.0] || leq(host(skc6),nbr_proc)*l -> equal(host(skc6),nbr_proc). % 43.89/44.07 1815[0:MRR:1709.0,8.0] || -> equal(host(skc6),nbr_proc)**. % 43.89/44.07 1818[0:Rew:1815.0,29.0] || equal(host(skc11),nbr_proc)** -> . % 43.89/44.07 1828[0:Rew:1815.0,679.0] || -> equal(head(snoc(queue(nbr_proc),u)),m_Down(skc7))**. % 43.89/44.07 1840[0:Rew:1815.0,132.0] || leq(index(pendack,host(skc11)),nbr_proc)*l -> . % 43.89/44.07 1859[0:Rew:1815.0,113.2] || leq(s(zero),u) -> equal(u,host(skc7)) setIn(u,index(down,nbr_proc))* leq(host(skc6),u). % 43.89/44.07 1910[0:Rew:1815.0,1859.3] || leq(s(zero),u) -> equal(u,host(skc7)) setIn(u,index(down,nbr_proc))* leq(nbr_proc,u). % 43.89/44.07 4424[0:EqR:805.0] || -> elem(head(snoc(u,v)),u)* equal(head(snoc(u,v)),v). % 43.89/44.07 4463[0:SpR:663.0,4424.0] || -> elem(u,cons(u,v))* equal(head(snoc(cons(u,v),w)),w)**. % 43.89/44.07 4481[0:Rew:663.0,4463.1] || -> elem(u,cons(u,v))* equal(u,w)*. % 43.89/44.07 6182[0:SpR:87.1,4481.0] || -> equal(u,q_nil) elem(head(u),u)* equal(head(u),v)*. % 43.89/44.07 7602[0:AED:9.0,6182.2] || -> equal(u,q_nil) elem(head(u),u)*. % 43.89/44.07 7864[0:SpR:1828.0,7602.1] || -> equal(snoc(queue(nbr_proc),u),q_nil) elem(m_Down(skc7),snoc(queue(nbr_proc),u))*. % 43.89/44.07 7886[0:MRR:7864.0,48.0] || -> elem(m_Down(skc7),snoc(queue(nbr_proc),u))*. % 43.89/44.07 7929[0:Res:7886.0,97.0] || -> elem(m_Down(skc7),queue(nbr_proc))* equal(m_Down(skc7),u)*. % 43.89/44.07 7930[0:AED:9.0,7929.1] || -> elem(m_Down(skc7),queue(nbr_proc))*. % 43.89/44.07 19155[0:SpL:1815.0,329.1] || setIn(skc6,alive) setIn(host(skc11),index(down,nbr_proc))* -> leq(index(pendack,host(skc11)),host(skc6)). % 43.89/44.07 19158[0:Rew:1815.0,19155.2] || setIn(skc6,alive) setIn(host(skc11),index(down,nbr_proc))* -> leq(index(pendack,host(skc11)),nbr_proc). % 43.89/44.07 19159[0:MRR:19158.0,19158.2,2.0,1840.0] || setIn(host(skc11),index(down,nbr_proc))* -> . % 43.89/44.07 19162[0:Res:1910.2,19159.0] || leq(s(zero),host(skc11))*l -> equal(host(skc11),host(skc7)) leq(nbr_proc,host(skc11)). % 43.89/44.07 19163[0:MRR:19162.0,24.0] || -> equal(host(skc11),host(skc7)) leq(nbr_proc,host(skc11))*r. % 43.89/44.07 34472[0:SpL:1815.0,352.1] || setIn(skc6,alive) elem(m_Down(u),queue(nbr_proc))* equal(host(skc11),host(u)) -> leq(index(pendack,host(skc11)),host(skc6)). % 43.89/44.07 34482[0:Rew:1815.0,34472.3] || setIn(skc6,alive) elem(m_Down(u),queue(nbr_proc))* equal(host(skc11),host(u)) -> leq(index(pendack,host(skc11)),nbr_proc). % 43.89/44.07 34483[0:MRR:34482.0,34482.3,2.0,1840.0] || elem(m_Down(u),queue(nbr_proc))* equal(host(skc11),host(u)) -> . % 43.89/44.07 42509[0:Res:7930.0,34483.0] || equal(host(skc11),host(skc7))** -> . % 43.89/44.07 42510[0:MRR:19163.0,42509.0] || -> leq(nbr_proc,host(skc11))*r. % 43.89/44.07 42986[0:Res:42510.0,94.0] || leq(host(skc11),nbr_proc)*l -> equal(host(skc11),nbr_proc). % 43.89/44.07 43472[0:MRR:42986.0,42986.1,8.0,1818.0] || -> . % 43.89/44.07 % SZS output end Refutation % 43.89/44.07 Formulae used in the proof : conj axiom_02 axiom_62 axiom_63 axiom_58 axiom_04 axiom_05 axiom_35 axiom_42 axiom_46 axiom_39 axiom_44 axiom_61 axiom_47 % 43.89/44.07 %------------------------------------------------------------------------------