%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV467+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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 100.90s 101.08s % Output : Refutation 102.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV467+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 15 08:29:48 EDT 2022 % 0.12/0.34 % CPUTime : % 100.90/101.08 % 100.90/101.08 SPASS V 3.9 % 100.90/101.08 SPASS beiseite: Proof found. % 100.90/101.08 % SZS status Theorem % 100.90/101.08 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.90/101.08 SPASS derived 56232 clauses, backtracked 1368 clauses, performed 14 splits and kept 19819 clauses. % 100.90/101.08 SPASS allocated 139746 KBytes. % 100.90/101.08 SPASS spent 0:1:40.66 on the problem. % 100.90/101.08 0:00:00.04 for the input. % 100.90/101.08 0:00:00.06 for the FLOTTER CNF translation. % 100.90/101.08 0:00:00.84 for inferences. % 100.90/101.08 0:00:00.84 for the backtracking. % 100.90/101.08 0:1:38.31 for the reduction. % 100.90/101.08 % 100.90/101.08 % 100.90/101.08 Here is a proof with depth 6, length 117 : % 100.90/101.08 % SZS output start Refutation % 100.90/101.08 3[0:Inp] || -> setIn(skc13,alive)*. % 100.90/101.08 6[0:Inp] || -> leq(nbr_proc,host(skc8))*r. % 100.90/101.08 8[0:Inp] || -> leq(host(u),nbr_proc)*l. % 100.90/101.08 9[0:Inp] || equal(elec_2,elec_1)** -> . % 100.90/101.08 16[0:Inp] || elem(u,q_nil)* -> . % 100.90/101.08 28[0:Inp] || leq(s(u),u)*l -> . % 100.90/101.08 29[0:Inp] || -> elem(m_Down(skc14),queue(host(skc13)))*. % 100.90/101.08 31[0:Inp] || -> equal(index(status__dfg,host(skc8)),elec_1)**. % 100.90/101.08 44[0:Inp] || -> equal(head(cons(u,v)),u)**. % 100.90/101.08 46[0:Inp] || -> equal(last(snoc(u,v)),v)**. % 100.90/101.08 47[0:Inp] || -> equal(init(snoc(u,v)),u)**. % 100.90/101.08 48[0:Inp] || equal(cons(u,v),q_nil)** -> . % 100.90/101.08 49[0:Inp] || equal(snoc(u,v),q_nil)** -> . % 100.90/101.08 50[0:Inp] || -> leq(u,v)* leq(v,u)*. % 100.90/101.08 51[0:Inp] || leq(host(u),skf5(v,u))*r -> . % 100.90/101.08 53[0:Inp] || -> leq(nbr_proc,s(index(pendack,host(skc13))))*r. % 100.90/101.08 54[0:Inp] || -> equal(index(pendack,host(skc13)),host(skc15))**. % 100.90/101.08 66[0:Inp] || equal(u,v)* -> leq(v,u). % 100.90/101.08 67[0:Inp] || -> equal(s(index(pendack,host(skc13))),host(skc14))**. % 100.90/101.08 68[0:Inp] || -> equal(cons(m_Down(skc9),skc10),queue(host(skc8)))**. % 100.90/101.08 81[0:Inp] || equal(u,v) -> elem(u,cons(v,w))*. % 100.90/101.08 83[0:Inp] || equal(u,v) -> elem(u,snoc(w,v))*. % 100.90/101.08 88[0:Inp] || leq(u,v) -> leq(s(u),s(v))*. % 100.90/101.08 91[0:Inp] || -> equal(u,q_nil) equal(cons(head(u),tail(u)),u)**. % 100.90/101.08 92[0:Inp] || -> equal(u,q_nil) equal(snoc(init(u),last(u)),u)**. % 100.90/101.08 97[0:Inp] || -> equal(cons(u,snoc(v,w)),snoc(cons(u,v),w))**. % 100.90/101.08 98[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 100.90/101.08 99[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 100.90/101.08 100[0:Inp] || elem(u,cons(v,w))* -> equal(u,v) elem(u,w). % 100.90/101.08 101[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 100.90/101.08 104[0:Inp] || leq(u,s(v))* -> leq(u,v) equal(u,s(v)). % 100.90/101.08 120[0:Inp] || leq(s(zero),u) -> equal(u,host(skc9)) setIn(u,index(down,host(skc8)))* leq(host(skc8),u). % 100.90/101.08 130[0:Inp] || setIn(u,alive) equal(host(v),nbr_proc) equal(host(v),host(w))* elem(m_Down(w),queue(host(u)))* elem(m_Down(x),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) -> leq(s(zero),skf5(x,v)). % 100.90/101.08 131[0:Inp] || setIn(u,alive) equal(host(v),nbr_proc) equal(host(v),host(w))* elem(m_Down(w),queue(host(u)))* elem(m_Down(x),queue(host(v)))* equal(skf5(x,v),host(x)) equal(index(status__dfg,host(v)),elec_1) -> . % 100.90/101.08 133[0:Inp] || setIn(u,alive) equal(host(v),nbr_proc) equal(host(v),host(w))* elem(m_Down(w),queue(host(u)))* elem(m_Down(x),queue(host(v))) setIn(skf5(x,v),index(down,host(v)))* equal(index(status__dfg,host(v)),elec_1) -> . % 100.90/101.08 136[0:Rew:54.0,67.0] || -> equal(s(host(skc15)),host(skc14))**. % 100.90/101.08 137[0:Rew:136.0,53.0,54.0,53.0] || -> leq(nbr_proc,host(skc14))*r. % 100.90/101.08 315[0:Res:29.0,130.4] || elem(m_Down(u),queue(host(v)))* equal(index(status__dfg,host(v)),elec_1) equal(host(v),nbr_proc) setIn(skc13,alive) equal(host(v),host(skc14)) -> leq(s(zero),skf5(u,v)). % 100.90/101.08 316[0:Res:29.0,133.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(skc13,alive) equal(host(v),host(skc14)) -> . % 100.90/101.08 317[0:Res:29.0,131.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(skc13,alive) equal(host(v),host(skc14)) -> . % 100.90/101.08 406[0:MRR:317.4,3.0] || equal(host(u),nbr_proc) equal(host(u),host(skc14)) elem(m_Down(v),queue(host(u)))* equal(skf5(v,u),host(v)) equal(index(status__dfg,host(u)),elec_1) -> . % 100.90/101.08 415[0:MRR:316.4,3.0] || equal(host(u),nbr_proc) equal(host(u),host(skc14)) elem(m_Down(v),queue(host(u))) setIn(skf5(v,u),index(down,host(u)))* equal(index(status__dfg,host(u)),elec_1) -> . % 100.90/101.08 422[0:MRR:315.3,3.0] || equal(host(u),nbr_proc) equal(host(u),host(skc14)) elem(m_Down(v),queue(host(u)))* equal(index(status__dfg,host(u)),elec_1) -> leq(s(zero),skf5(v,u)). % 100.90/101.08 499[0:SpR:68.0,44.0] || -> equal(head(queue(host(skc8))),m_Down(skc9))**. % 100.90/101.08 714[0:SpR:92.1,83.1] || equal(u,last(v)) -> equal(v,q_nil) elem(u,v)*. % 100.90/101.08 734[0:SpR:91.1,81.1] || equal(u,head(v)) -> equal(v,q_nil) elem(u,v)*. % 100.90/101.08 778[0:SpR:97.0,44.0] || -> equal(head(snoc(cons(u,v),w)),u)**. % 100.90/101.08 782[0:SpR:92.1,97.0] || -> equal(u,q_nil) equal(snoc(cons(v,init(u)),last(u)),cons(v,u))**. % 100.90/101.08 794[0:SpR:68.0,778.0] || -> equal(head(snoc(queue(host(skc8)),u)),m_Down(skc9))**. % 100.90/101.08 941[0:Res:714.2,100.0] || equal(u,last(cons(v,w)))* -> equal(cons(v,w),q_nil) equal(u,v) elem(u,w)*. % 100.90/101.08 954[0:MRR:941.1,48.0] || equal(u,last(cons(v,w)))*+ -> equal(u,v) elem(u,w)*. % 100.90/101.08 1047[0:Res:734.2,101.0] || equal(u,head(snoc(v,w)))* -> equal(snoc(v,w),q_nil) elem(u,v)* equal(u,w). % 100.90/101.08 1063[0:MRR:1047.1,49.0] || equal(u,head(snoc(v,w)))*+ -> elem(u,v)* equal(u,w). % 100.90/101.08 1158[0:NCh:99.2,99.1,50.1,51.0] || leq(host(u),v)*+ -> leq(skf5(w,u),v)*. % 100.90/101.08 1518[0:NCh:99.2,99.0,88.1,28.0] || leq(u,v)*+ equal(s(v),u)* -> . % 100.90/101.08 1796[0:Res:6.0,98.0] || leq(host(skc8),nbr_proc)*l -> equal(host(skc8),nbr_proc). % 100.90/101.08 1797[0:Res:137.0,98.0] || leq(host(skc14),nbr_proc)*l -> equal(host(skc14),nbr_proc). % 100.90/101.08 1899[0:MRR:1796.0,8.0] || -> equal(host(skc8),nbr_proc)**. % 100.90/101.08 1900[0:Rew:1899.0,31.0] || -> equal(index(status__dfg,nbr_proc),elec_1)**. % 100.90/101.08 1910[0:Rew:1899.0,499.0] || -> equal(head(queue(nbr_proc)),m_Down(skc9))**. % 100.90/101.08 1916[0:Rew:1899.0,794.0] || -> equal(head(snoc(queue(nbr_proc),u)),m_Down(skc9))**. % 100.90/101.08 1951[0:Rew:1899.0,120.2] || leq(s(zero),u) -> equal(u,host(skc9)) setIn(u,index(down,nbr_proc))* leq(host(skc8),u). % 100.90/101.08 1984[0:MRR:1797.0,8.0] || -> equal(host(skc14),nbr_proc)**. % 100.90/101.08 1985[0:Rew:1984.0,136.0] || -> equal(s(host(skc15)),nbr_proc)**. % 100.90/101.08 2010[0:Rew:1984.0,422.1] || equal(host(u),nbr_proc) 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)). % 100.90/101.08 2011[0:Rew:1984.0,415.1] || equal(host(u),nbr_proc) 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) -> . % 100.90/101.08 2012[0:Rew:1984.0,406.1] || equal(host(u),nbr_proc) 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) -> . % 100.90/101.08 2102[0:Rew:1899.0,1951.3] || leq(s(zero),u) -> equal(u,host(skc9)) setIn(u,index(down,nbr_proc))* leq(nbr_proc,u). % 100.90/101.08 2107[0:Obv:2012.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) -> . % 100.90/101.08 2110[0:Obv:2011.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) -> . % 100.90/101.08 2113[0:Obv:2010.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)). % 100.90/101.08 2245[0:SpL:1985.0,104.0] || leq(u,nbr_proc)* -> leq(u,host(skc15))* equal(u,s(host(skc15)))*. % 100.90/101.08 2259[0:Res:50.0,104.0] || -> leq(s(u),v)* leq(v,u)* equal(v,s(u)). % 100.90/101.08 2307[0:MRR:2259.2,66.0] || -> leq(s(u),v)* leq(v,u)*. % 100.90/101.08 2308[0:Rew:1985.0,2245.2] || leq(u,nbr_proc)*+ -> leq(u,host(skc15))* equal(u,nbr_proc). % 100.90/101.08 5440[0:SpR:782.1,47.0] || -> equal(u,q_nil) equal(cons(v,init(u)),init(cons(v,u)))**. % 100.90/101.08 6386[0:NCh:99.2,99.1,2307.0,51.0] || equal(host(u),s(v))*+ -> leq(skf5(w,u),v)*. % 100.90/101.08 7417[0:SpR:5440.1,44.0] || -> equal(u,q_nil) equal(head(init(cons(v,u))),v)**. % 100.90/101.08 7587[0:SpR:91.1,7417.1] || -> equal(u,q_nil) equal(tail(u),q_nil) equal(head(init(u)),head(u))**. % 100.90/101.08 9895[0:Res:8.0,1158.0] || -> leq(skf5(u,v),nbr_proc)*l. % 100.90/101.08 10030[0:Res:9895.0,98.0] || leq(nbr_proc,skf5(u,v))*r -> equal(skf5(u,v),nbr_proc). % 100.90/101.08 10175[0:Res:8.0,2308.0] || -> leq(host(u),host(skc15))* equal(host(u),nbr_proc)**. % 100.90/101.08 15380[0:SpR:47.0,7587.2] || -> equal(snoc(u,v),q_nil) equal(tail(snoc(u,v)),q_nil)** equal(head(snoc(u,v)),head(u)). % 100.90/101.08 15387[0:MRR:15380.0,49.0] || -> equal(tail(snoc(u,v)),q_nil)** equal(head(snoc(u,v)),head(u)). % 100.90/101.08 16809[0:EqR:954.0] || -> equal(last(cons(u,v)),u) elem(last(cons(u,v)),v)*. % 100.90/101.08 16829[0:SpR:91.1,16809.1] || -> equal(u,q_nil) equal(last(cons(head(u),tail(u))),head(u))** elem(last(u),tail(u)). % 100.90/101.08 16847[0:Rew:91.1,16829.1] || -> equal(u,q_nil) equal(last(u),head(u)) elem(last(u),tail(u))*. % 102.83/103.00 21507[0:SpR:15387.0,16847.2] || -> equal(head(snoc(u,v)),head(u)) equal(snoc(u,v),q_nil) equal(last(snoc(u,v)),head(snoc(u,v))) elem(last(snoc(u,v)),q_nil)*. % 102.83/103.00 21540[0:Rew:46.0,21507.3,46.0,21507.2] || -> equal(head(snoc(u,v)),head(u))** equal(snoc(u,v),q_nil) equal(head(snoc(u,v)),v)** elem(v,q_nil). % 102.83/103.00 21541[0:MRR:21540.1,21540.3,49.0,16.0] || -> equal(head(snoc(u,v)),head(u))** equal(head(snoc(u,v)),v)**. % 102.83/103.00 22906[0:SpL:1984.0,2107.1] || equal(host(skc14),nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc14),host(u)) equal(index(status__dfg,host(skc14)),elec_1) -> . % 102.83/103.00 22916[0:Rew:1900.0,22906.3,1984.0,22906.3,1984.0,22906.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc14),host(u)) equal(elec_1,elec_1) -> . % 102.83/103.00 22917[0:Obv:22916.3] || elem(m_Down(u),queue(nbr_proc))* equal(skf5(u,skc14),host(u)) -> . % 102.83/103.00 27381[0:SpL:1984.0,2110.2] || equal(host(skc14),nbr_proc) elem(m_Down(u),queue(host(skc14))) setIn(skf5(u,skc14),index(down,nbr_proc))* equal(index(status__dfg,host(skc14)),elec_1) -> . % 102.83/103.00 27384[0:Rew:1900.0,27381.3,1984.0,27381.3,1984.0,27381.1,1984.0,27381.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc)) setIn(skf5(u,skc14),index(down,nbr_proc))* equal(elec_1,elec_1) -> . % 102.83/103.00 27385[0:Obv:27384.3] || elem(m_Down(u),queue(nbr_proc)) setIn(skf5(u,skc14),index(down,nbr_proc))* -> . % 102.83/103.00 32330[0:SpL:1984.0,2113.1] || equal(host(skc14),nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(index(status__dfg,host(skc14)),elec_1) -> leq(s(zero),skf5(u,skc14)). % 102.83/103.00 32342[0:Rew:1900.0,32330.2,1984.0,32330.2,1984.0,32330.0] || equal(nbr_proc,nbr_proc) elem(m_Down(u),queue(nbr_proc))* equal(elec_1,elec_1) -> leq(s(zero),skf5(u,skc14)). % 102.83/103.00 32343[0:Obv:32342.2] || elem(m_Down(u),queue(nbr_proc))* -> leq(s(zero),skf5(u,skc14)). % 102.83/103.00 41845[0:EqR:1063.0] || -> elem(head(snoc(u,v)),u)* equal(head(snoc(u,v)),v). % 102.83/103.00 41880[0:Rew:21541.0,41845.0] || -> elem(head(u),u)* equal(head(snoc(u,v)),v)**. % 102.83/103.00 41939[0:SpR:41880.1,1916.0] || -> elem(head(queue(nbr_proc)),queue(nbr_proc))* equal(u,m_Down(skc9))*. % 102.83/103.00 42010[0:AED:9.0,41939.1] || -> elem(head(queue(nbr_proc)),queue(nbr_proc))*. % 102.83/103.00 42011[0:Rew:1910.0,42010.0] || -> elem(m_Down(skc9),queue(nbr_proc))*. % 102.83/103.00 44883[0:Res:10175.0,1158.0] || -> equal(host(u),nbr_proc) leq(skf5(v,u),host(skc15))*l. % 102.83/103.00 45484[0:Res:2102.2,27385.1] || leq(s(zero),skf5(u,skc14)) elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc14),host(skc9)) leq(nbr_proc,skf5(u,skc14)). % 102.83/103.00 45485[0:MRR:45484.0,32343.1] || elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc14),host(skc9)) leq(nbr_proc,skf5(u,skc14)). % 102.83/103.00 70475[0:SpL:1985.0,6386.0] || equal(host(u),nbr_proc) -> leq(skf5(v,u),host(skc15))*l. % 102.83/103.00 70478[0:Rew:44883.0,70475.0] || equal(nbr_proc,nbr_proc) -> leq(skf5(u,v),host(skc15))*l. % 102.83/103.00 70479[0:Obv:70478.0] || -> leq(skf5(u,v),host(skc15))*l. % 102.83/103.00 70493[0:Res:70479.0,1518.0] || equal(skf5(u,v),s(host(skc15)))** -> . % 102.83/103.00 70586[0:Rew:1985.0,70493.0] || equal(skf5(u,v),nbr_proc)** -> . % 102.83/103.00 70587[0:MRR:10030.1,70586.0] || leq(nbr_proc,skf5(u,v))*r -> . % 102.83/103.00 70589[0:MRR:45485.2,70587.0] || elem(m_Down(u),queue(nbr_proc))* -> equal(skf5(u,skc14),host(skc9)). % 102.83/103.00 70593[0:Rew:70589.1,22917.1] || elem(m_Down(u),queue(nbr_proc))* equal(host(skc9),host(u)) -> . % 102.83/103.00 71432[0:Res:42011.0,70593.0] || equal(host(skc9),host(skc9))* -> . % 102.83/103.00 71435[0:Obv:71432.0] || -> . % 102.83/103.00 % SZS output end Refutation % 102.83/103.00 Formulae used in the proof : conj axiom_02 axiom_62 axiom_63 axiom_58 axiom_04 axiom_05 axiom_45 axiom_35 axiom_37 axiom_38 axiom_41 axiom_42 axiom_60 axiom_61 axiom_46 axiom_47 axiom_39 axiom_40 axiom_44 axiom_64 % 102.83/103.00 %------------------------------------------------------------------------------