%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV466+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:11 EDT 2022 % Result : Theorem 65.45s 65.67s % Output : Refutation 65.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV466+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.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 20:20:11 EDT 2022 % 0.13/0.35 % CPUTime : % 65.45/65.67 % 65.45/65.67 SPASS V 3.9 % 65.45/65.67 SPASS beiseite: Proof found. % 65.45/65.67 % SZS status Theorem % 65.45/65.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 65.45/65.67 SPASS derived 38268 clauses, backtracked 6 clauses, performed 11 splits and kept 15378 clauses. % 65.45/65.67 SPASS allocated 126849 KBytes. % 65.45/65.67 SPASS spent 0:01:04.34 on the problem. % 65.45/65.67 0:00:00.04 for the input. % 65.45/65.67 0:00:00.06 for the FLOTTER CNF translation. % 65.45/65.67 0:00:00.58 for inferences. % 65.45/65.67 0:00:00.64 for the backtracking. % 65.45/65.67 0:01:02.60 for the reduction. % 65.45/65.67 % 65.45/65.67 % 65.45/65.67 Here is a proof with depth 4, length 75 : % 65.45/65.67 % SZS output start Refutation % 65.45/65.67 2[0:Inp] || -> setIn(skc8,alive)*. % 65.45/65.67 3[0:Inp] || -> setIn(skc13,alive)*. % 65.45/65.67 7[0:Inp] || -> leq(host(u),nbr_proc)*l. % 65.45/65.67 23[0:Inp] || -> equal(host(skc13),host(skc11))**. % 65.45/65.67 29[0:Inp] || -> equal(index(status__dfg,host(skc8)),elec_2)**. % 65.45/65.67 30[0:Inp] || -> leq(nbr_proc,index(pendack,host(skc8)))*r. % 65.45/65.67 31[0:Inp] || equal(host(skc13),host(skc8))** -> . % 65.45/65.67 32[0:Inp] || -> equal(index(status__dfg,host(skc13)),elec_2)**. % 65.45/65.67 52[0:Inp] || -> equal(index(pendack,host(skc8)),host(skc9))**. % 65.45/65.67 53[0:Inp] || -> leq(nbr_proc,s(index(pendack,host(skc13))))*r. % 65.45/65.67 54[0:Inp] || -> equal(index(pendack,host(skc13)),host(skc15))**. % 65.45/65.67 58[0:Inp] || equal(m_Ack(u,v),m_Ldr(w))* -> . % 65.45/65.67 67[0:Inp] || -> equal(s(index(pendack,host(skc13))),host(skc14))**. % 65.45/65.67 68[0:Inp] || -> equal(cons(m_Down(skc9),skc10),queue(host(skc8)))**. % 65.45/65.67 82[0:Inp] || equal(u,v) -> elem(u,cons(v,w))*. % 65.45/65.67 92[0:Inp] || -> elem(m_Ack(skc13,skc15),snoc(queue(host(skc13)),m_Ldr(skc8)))*. % 65.45/65.67 100[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 65.45/65.67 101[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 65.45/65.67 103[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 65.45/65.67 106[0:Inp] || leq(u,s(v))* -> leq(u,v) equal(u,s(v)). % 65.45/65.67 108[0:Inp] || equal(host(u),host(v)) elem(m_Down(u),queue(host(v)))* -> . % 65.45/65.67 112[0:Inp] || leq(host(u),host(v)) elem(m_Ack(v,u),queue(host(w)))* -> . % 65.45/65.67 125[0:Inp] || setIn(u,alive) setIn(v,alive) equal(index(status__dfg,host(u)),elec_2)**+ equal(index(status__dfg,host(v)),elec_2)** -> leq(host(v),host(u))* leq(index(pendack,host(u)),host(v))*. % 65.45/65.67 127[0:Inp] || setIn(u,alive) setIn(v,alive) equal(host(u),host(w))* elem(m_Ack(v,w),queue(host(v)))*+ equal(index(status__dfg,host(u)),elec_2)** equal(index(status__dfg,host(v)),elec_2) -> . % 65.45/65.67 134[0:Rew:23.0,32.0] || -> equal(index(status__dfg,host(skc11)),elec_2)**. % 65.45/65.67 135[0:Rew:23.0,31.0] || equal(host(skc11),host(skc8))** -> . % 65.45/65.67 137[0:Rew:23.0,54.0] || -> equal(index(pendack,host(skc11)),host(skc15))**. % 65.45/65.67 138[0:Rew:137.0,67.0,23.0,67.0] || -> equal(s(host(skc15)),host(skc14))**. % 65.45/65.67 140[0:Rew:23.0,92.0] || -> elem(m_Ack(skc13,skc15),snoc(queue(host(skc11)),m_Ldr(skc8)))*. % 65.45/65.67 141[0:Rew:52.0,30.0] || -> leq(nbr_proc,host(skc9))*r. % 65.45/65.67 142[0:Rew:138.0,53.0,137.0,53.0,23.0,53.0] || -> leq(nbr_proc,host(skc14))*r. % 65.45/65.67 166[0:Res:3.0,125.3] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** equal(index(status__dfg,host(skc13)),elec_2)** -> leq(host(u),host(skc13)) leq(index(pendack,host(skc13)),host(u)). % 65.45/65.67 310[0:Res:100.2,135.0] || leq(host(skc11),host(skc8))*l leq(host(skc8),host(skc11)) -> . % 65.45/65.67 326[0:Res:29.0,127.5] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2) elem(m_Ack(u,v),queue(host(u)))* equal(host(skc8),host(v)) setIn(skc8,alive) -> . % 65.45/65.67 329[0:Res:29.0,125.2] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** setIn(skc8,alive) -> leq(host(u),host(skc8)) leq(index(pendack,host(skc8)),host(u)). % 65.45/65.67 388[0:MRR:326.4,2.0] || setIn(u,alive) equal(host(skc8),host(v)) elem(m_Ack(u,v),queue(host(u)))* equal(index(status__dfg,host(u)),elec_2) -> . % 65.45/65.67 415[0:Rew:52.0,329.4] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** setIn(skc8,alive) -> leq(host(u),host(skc8)) leq(host(skc9),host(u)). % 65.45/65.67 416[0:MRR:415.2,2.0] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** -> leq(host(u),host(skc8)) leq(host(skc9),host(u)). % 65.45/65.67 439[0:Rew:137.0,166.4,23.0,166.4,23.0,166.3,134.0,166.2,23.0,166.2] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** equal(elec_2,elec_2) -> leq(host(u),host(skc11)) leq(host(skc15),host(u)). % 65.45/65.67 440[0:Obv:439.2] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** -> leq(host(u),host(skc11)) leq(host(skc15),host(u)). % 65.45/65.67 724[0:SpR:68.0,82.1] || equal(u,m_Down(skc9)) -> elem(u,queue(host(skc8)))*. % 65.45/65.67 924[0:Res:140.0,103.0] || -> elem(m_Ack(skc13,skc15),queue(host(skc11)))* equal(m_Ack(skc13,skc15),m_Ldr(skc8)). % 65.45/65.67 934[0:MRR:924.1,58.0] || -> elem(m_Ack(skc13,skc15),queue(host(skc11)))*. % 65.45/65.67 1005[0:Res:724.1,108.1] || equal(m_Down(u),m_Down(skc9)) equal(host(u),host(skc8))* -> . % 65.45/65.67 1743[0:Res:934.0,112.1] || leq(host(skc15),host(skc13))*l -> . % 65.45/65.67 1744[0:Rew:23.0,1743.0] || leq(host(skc15),host(skc11))*l -> . % 65.45/65.67 1749[0:NCh:101.2,101.0,1744.0,7.0] || leq(nbr_proc,host(skc11))*r -> . % 65.45/65.67 1843[0:Res:141.0,100.0] || leq(host(skc9),nbr_proc)*l -> equal(host(skc9),nbr_proc). % 65.45/65.67 1844[0:Res:142.0,100.0] || leq(host(skc14),nbr_proc)*l -> equal(host(skc14),nbr_proc). % 65.45/65.67 1949[0:MRR:1843.0,7.0] || -> equal(host(skc9),nbr_proc)**. % 65.45/65.67 1957[0:Rew:1949.0,416.3] || setIn(u,alive) equal(index(status__dfg,host(u)),elec_2)** -> leq(host(u),host(skc8)) leq(nbr_proc,host(u)). % 65.45/65.67 1990[0:MRR:1844.0,7.0] || -> equal(host(skc14),nbr_proc)**. % 65.45/65.67 1991[0:Rew:1990.0,138.0] || -> equal(s(host(skc15)),nbr_proc)**. % 65.45/65.67 2109[0:SpL:1949.0,1005.1] || equal(m_Down(skc9),m_Down(skc9)) equal(host(skc8),nbr_proc)** -> . % 65.45/65.67 2113[0:Obv:2109.0] || equal(host(skc8),nbr_proc)** -> . % 65.45/65.67 2182[0:SpL:1991.0,106.0] || leq(u,nbr_proc)* -> leq(u,host(skc15))* equal(u,s(host(skc15)))*. % 65.45/65.67 2245[0:Rew:1991.0,2182.2] || leq(u,nbr_proc)*+ -> leq(u,host(skc15))* equal(u,nbr_proc). % 65.45/65.67 10879[0:Res:7.0,2245.0] || -> leq(host(u),host(skc15))* equal(host(u),nbr_proc)**. % 65.45/65.67 18699[0:SpL:23.0,388.2] || setIn(skc13,alive) equal(host(skc8),host(u)) elem(m_Ack(skc13,u),queue(host(skc11)))* equal(index(status__dfg,host(skc13)),elec_2) -> . % 65.45/65.67 18709[0:Rew:134.0,18699.3,23.0,18699.3] || setIn(skc13,alive) equal(host(skc8),host(u)) elem(m_Ack(skc13,u),queue(host(skc11)))* equal(elec_2,elec_2) -> . % 65.45/65.67 18710[0:Obv:18709.3] || setIn(skc13,alive) equal(host(skc8),host(u)) elem(m_Ack(skc13,u),queue(host(skc11)))* -> . % 65.45/65.67 18711[0:MRR:18710.0,3.0] || equal(host(skc8),host(u)) elem(m_Ack(skc13,u),queue(host(skc11)))* -> . % 65.45/65.67 30285[0:SpL:23.0,1957.1] || setIn(skc13,alive) equal(index(status__dfg,host(skc11)),elec_2)** -> leq(host(skc13),host(skc8)) leq(nbr_proc,host(skc13)). % 65.45/65.67 30297[0:Rew:23.0,30285.3,23.0,30285.2,134.0,30285.1] || setIn(skc13,alive)* equal(elec_2,elec_2) -> leq(host(skc11),host(skc8)) leq(nbr_proc,host(skc11)). % 65.45/65.67 30298[0:Obv:30297.1] || setIn(skc13,alive)* -> leq(host(skc11),host(skc8)) leq(nbr_proc,host(skc11)). % 65.45/65.67 30299[0:MRR:30298.0,30298.2,3.0,1749.0] || -> leq(host(skc11),host(skc8))*l. % 65.45/65.67 30300[0:MRR:310.0,30299.0] || leq(host(skc8),host(skc11))*r -> . % 65.45/65.67 30735[0:SpL:29.0,440.1] || setIn(skc8,alive)* equal(elec_2,elec_2) -> leq(host(skc8),host(skc11)) leq(host(skc15),host(skc8)). % 65.45/65.67 30736[0:Obv:30735.1] || setIn(skc8,alive)* -> leq(host(skc8),host(skc11)) leq(host(skc15),host(skc8)). % 65.45/65.67 30737[0:MRR:30736.0,30736.1,2.0,30300.0] || -> leq(host(skc15),host(skc8))*l. % 65.45/65.67 30764[0:Res:30737.0,100.0] || leq(host(skc8),host(skc15))*r -> equal(host(skc15),host(skc8)). % 65.45/65.67 46857[0:Res:934.0,18711.1] || equal(host(skc15),host(skc8))** -> . % 65.45/65.67 46858[0:MRR:30764.1,46857.0] || leq(host(skc8),host(skc15))*r -> . % 65.45/65.67 46863[0:Res:10879.0,46858.0] || -> equal(host(skc8),nbr_proc)**. % 65.45/65.67 46893[0:MRR:46863.0,2113.0] || -> . % 65.45/65.67 % SZS output end Refutation % 65.45/65.67 Formulae used in the proof : conj axiom_02 axiom_62 axiom_63 axiom_58 axiom_04 axiom_14 axiom_46 axiom_61 axiom_47 axiom_64 % 65.45/65.67 %------------------------------------------------------------------------------