%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV449+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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:08 EDT 2022 % Result : Theorem 32.81s 33.01s % Output : Refutation 32.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV449+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n010.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 17:20:39 EDT 2022 % 0.12/0.34 % CPUTime : % 32.81/33.01 % 32.81/33.01 SPASS V 3.9 % 32.81/33.01 SPASS beiseite: Proof found. % 32.81/33.01 % SZS status Theorem % 32.81/33.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 32.81/33.01 SPASS derived 25939 clauses, backtracked 606 clauses, performed 17 splits and kept 12426 clauses. % 32.81/33.01 SPASS allocated 114942 KBytes. % 32.81/33.01 SPASS spent 0:0:32.52 on the problem. % 32.81/33.01 0:00:00.04 for the input. % 32.81/33.01 0:00:00.05 for the FLOTTER CNF translation. % 32.81/33.01 0:00:00.32 for inferences. % 32.81/33.01 0:00:00.26 for the backtracking. % 32.81/33.01 0:0:31.68 for the reduction. % 32.81/33.01 % 32.81/33.01 % 32.81/33.01 Here is a proof with depth 5, length 78 : % 32.81/33.01 % SZS output start Refutation % 32.81/33.01 3[0:Inp] || -> setIn(skc13,alive)*. % 32.81/33.01 4[0:Inp] || -> setIn(skc8,alive)*. % 32.81/33.01 7[0:Inp] || -> leq(host(u),nbr_proc)*l. % 32.81/33.01 15[0:Inp] || elem(u,q_nil)* -> . % 32.81/33.01 21[0:Inp] || -> equal(host(skc15),host(skc12))**. % 32.81/33.01 22[0:Inp] || -> equal(host(skc14),host(skc13))**. % 32.81/33.01 23[0:Inp] || -> equal(host(skc12),host(skc11))**. % 32.81/33.01 24[0:Inp] || -> equal(host(skc12),host(skc8))**. % 32.81/33.01 31[0:Inp] || -> elem(m_Down(skc15),queue(host(skc13)))*. % 32.81/33.01 33[0:Inp] || equal(host(skc13),host(skc11))** -> . % 32.81/33.01 35[0:Inp] || -> leq(nbr_proc,index(pendack,host(skc8)))*r. % 32.81/33.01 38[0:Inp] || equal(m_Down(u),m_Ldr(v))* -> . % 32.81/33.01 53[0:Inp] || -> elem(m_Down(skc14),snoc(skc10,m_Ldr(skc8)))*. % 32.81/33.01 54[0:Inp] || -> equal(index(pendack,host(skc8)),host(skc9))**. % 32.81/33.01 80[0:Inp] || elem(u,v) -> elem(u,cons(w,v))*. % 32.81/33.01 81[0:Inp] || equal(u,v) -> elem(u,snoc(w,v))*. % 32.81/33.01 90[0:Inp] || -> equal(u,q_nil) equal(snoc(init(u),last(u)),u)**. % 32.81/33.01 92[0:Inp] || elem(m_Ack(u,v),queue(host(u)))* -> setIn(u,pids). % 32.81/33.01 97[0:Inp] || leq(u,v)*+ leq(v,u)* -> equal(v,u). % 32.81/33.01 99[0:Inp] || -> setIn(host(skc11),index(acks,host(skc8)))* equal(host(skc11),host(skc9)). % 32.81/33.01 100[0:Inp] || -> equal(cons(m_Ack(index(elid,host(skc8)),skc9),skc10),queue(host(skc8)))**. % 32.81/33.01 102[0:Inp] || elem(u,snoc(v,w))* -> elem(u,v) equal(u,w). % 32.81/33.01 120[0:Inp] || setIn(u,alive) setIn(v,alive) equal(host(w),host(u))* equal(host(x),host(v))* elem(m_Down(x),queue(host(u)))*+ elem(m_Down(w),queue(host(v)))* -> equal(host(u),host(v))*. % 32.81/33.01 121[0:Rew:24.0,23.0] || -> equal(host(skc11),host(skc8))**. % 32.81/33.01 122[0:Rew:24.0,21.0] || -> equal(host(skc15),host(skc8))**. % 32.81/33.01 123[0:Rew:121.0,33.0] || equal(host(skc13),host(skc8))** -> . % 32.81/33.01 126[0:Rew:54.0,35.0] || -> leq(nbr_proc,host(skc9))*r. % 32.81/33.01 127[0:Rew:121.0,99.1,121.0,99.0] || -> setIn(host(skc8),index(acks,host(skc8)))* equal(host(skc9),host(skc8)). % 32.81/33.01 294[0:Res:120.6,123.0] || setIn(skc13,alive) equal(host(u),host(skc13)) elem(m_Down(v),queue(host(skc13)))* elem(m_Down(u),queue(host(skc8)))* equal(host(v),host(skc8)) setIn(skc8,alive) -> . % 32.81/33.01 314[0:Res:31.0,120.3] || setIn(u,alive) equal(host(skc15),host(u)) elem(m_Down(v),queue(host(u)))* equal(host(v),host(skc13)) setIn(skc13,alive) -> equal(host(skc13),host(u)). % 32.81/33.01 333[0:Res:53.0,102.0] || -> elem(m_Down(skc14),skc10)* equal(m_Ldr(skc8),m_Down(skc14)). % 32.81/33.01 337[0:Res:126.0,97.1] || leq(host(skc9),nbr_proc)*l -> equal(host(skc9),nbr_proc). % 32.81/33.01 405[0:MRR:337.0,7.0] || -> equal(host(skc9),nbr_proc)**. % 32.81/33.01 408[0:Rew:405.0,127.1] || -> equal(host(skc8),nbr_proc) setIn(host(skc8),index(acks,host(skc8)))*. % 32.81/33.01 423[0:Rew:122.0,314.1] || setIn(u,alive) equal(host(skc8),host(u)) elem(m_Down(v),queue(host(u)))* equal(host(v),host(skc13)) setIn(skc13,alive) -> equal(host(skc13),host(u)). % 32.81/33.01 424[0:MRR:423.4,3.0] || setIn(u,alive) equal(host(v),host(skc13)) elem(m_Down(v),queue(host(u)))* equal(host(skc8),host(u)) -> equal(host(skc13),host(u)). % 32.81/33.01 431[0:MRR:294.0,294.5,3.0,4.0] || equal(host(u),host(skc8)) equal(host(v),host(skc13)) elem(m_Down(v),queue(host(skc8)))*+ elem(m_Down(u),queue(host(skc13)))* -> . % 32.81/33.01 434[1:Spt:408.0] || -> equal(host(skc8),nbr_proc)**. % 32.81/33.01 438[1:Rew:434.0,431.2] || equal(host(u),host(skc8)) equal(host(v),host(skc13)) elem(m_Down(v),queue(nbr_proc))* elem(m_Down(u),queue(host(skc13)))* -> . % 32.81/33.01 447[1:Rew:434.0,122.0] || -> equal(host(skc15),nbr_proc)**. % 32.81/33.01 452[1:Rew:434.0,100.0] || -> equal(cons(m_Ack(index(elid,nbr_proc),skc9),skc10),queue(nbr_proc))**. % 32.81/33.01 456[1:Rew:434.0,438.0] || equal(host(u),nbr_proc) equal(host(v),host(skc13)) elem(m_Down(v),queue(nbr_proc))* elem(m_Down(u),queue(host(skc13)))*+ -> . % 32.81/33.01 709[1:SpR:452.0,80.1] || elem(u,skc10) -> elem(u,queue(nbr_proc))*. % 32.81/33.01 762[0:SpR:90.1,81.1] || equal(u,last(v)) -> equal(v,q_nil) elem(u,v)*. % 32.81/33.01 855[1:SpL:434.0,92.0] || elem(m_Ack(skc8,u),queue(nbr_proc))* -> setIn(skc8,pids). % 32.81/33.01 1005[1:Res:709.1,855.0] || elem(m_Ack(skc8,u),skc10)* -> setIn(skc8,pids). % 32.81/33.01 2082[1:Res:762.2,1005.0] || equal(m_Ack(skc8,u),last(skc10))** -> equal(skc10,q_nil) setIn(skc8,pids). % 32.81/33.01 2946[2:Spt:2082.1] || -> equal(skc10,q_nil)**. % 32.81/33.01 2949[2:Rew:2946.0,333.0] || -> elem(m_Down(skc14),q_nil)* equal(m_Ldr(skc8),m_Down(skc14)). % 32.81/33.01 3007[2:MRR:2949.0,15.0] || -> equal(m_Ldr(skc8),m_Down(skc14))**. % 32.81/33.01 3008[2:UnC:3007.0,38.0] || -> . % 32.81/33.01 3021[2:Spt:3008.0,2082.1,2946.0] || equal(skc10,q_nil)** -> . % 32.81/33.01 3022[2:Spt:3008.0,2082.0,2082.2] || equal(m_Ack(skc8,u),last(skc10))** -> setIn(skc8,pids). % 32.81/33.01 3118[3:Spt:333.1] || -> equal(m_Ldr(skc8),m_Down(skc14))**. % 32.81/33.01 3119[3:UnC:3118.0,38.0] || -> . % 32.81/33.01 3120[3:Spt:3119.0,333.1,3118.0] || equal(m_Ldr(skc8),m_Down(skc14))** -> . % 32.81/33.01 3121[3:Spt:3119.0,333.0] || -> elem(m_Down(skc14),skc10)*. % 32.81/33.01 4997[0:Res:53.0,102.0] || -> elem(m_Down(skc14),skc10)* equal(m_Ldr(skc8),m_Down(skc14)). % 32.81/33.01 14739[1:Res:31.0,456.3] || equal(host(skc15),nbr_proc) equal(host(u),host(skc13)) elem(m_Down(u),queue(nbr_proc))* -> . % 32.81/33.01 14741[1:Rew:447.0,14739.0] || equal(nbr_proc,nbr_proc) equal(host(u),host(skc13)) elem(m_Down(u),queue(nbr_proc))* -> . % 32.81/33.01 14742[1:Obv:14741.0] || equal(host(u),host(skc13)) elem(m_Down(u),queue(nbr_proc))* -> . % 32.81/33.01 14759[1:Res:709.1,14742.1] || elem(m_Down(u),skc10)* equal(host(u),host(skc13)) -> . % 32.81/33.01 14767[3:Res:3121.0,14759.0] || equal(host(skc14),host(skc13))** -> . % 32.81/33.01 14769[3:Rew:22.0,14767.0] || equal(host(skc13),host(skc13))* -> . % 32.81/33.01 14770[3:Obv:14769.0] || -> . % 32.81/33.01 14773[1:Spt:14770.0,408.0,434.0] || equal(host(skc8),nbr_proc)** -> . % 32.81/33.01 14774[1:Spt:14770.0,408.1] || -> setIn(host(skc8),index(acks,host(skc8)))*. % 32.81/33.01 15003[0:SpR:100.0,80.1] || elem(u,skc10) -> elem(u,queue(host(skc8)))*. % 32.81/33.01 15096[2:Spt:4997.1] || -> equal(m_Ldr(skc8),m_Down(skc14))**. % 32.81/33.01 15097[2:UnC:15096.0,38.0] || -> . % 32.81/33.01 15098[2:Spt:15097.0,4997.1,15096.0] || equal(m_Ldr(skc8),m_Down(skc14))** -> . % 32.81/33.01 15099[2:Spt:15097.0,4997.0] || -> elem(m_Down(skc14),skc10)*. % 32.81/33.01 24822[0:Res:15003.1,424.2] || elem(m_Down(u),skc10)* setIn(skc8,alive) equal(host(u),host(skc13)) equal(host(skc8),host(skc8)) -> equal(host(skc13),host(skc8)). % 32.81/33.01 24824[0:Obv:24822.3] || elem(m_Down(u),skc10)* setIn(skc8,alive) equal(host(u),host(skc13)) -> equal(host(skc13),host(skc8)). % 32.81/33.01 24825[0:MRR:24824.1,24824.3,4.0,123.0] || elem(m_Down(u),skc10)* equal(host(u),host(skc13)) -> . % 32.81/33.01 28119[2:Res:15099.0,24825.0] || equal(host(skc14),host(skc13))** -> . % 32.81/33.01 28121[2:Rew:22.0,28119.0] || equal(host(skc13),host(skc13))* -> . % 32.81/33.01 28122[2:Obv:28121.0] || -> . % 32.81/33.01 % SZS output end Refutation % 32.81/33.01 Formulae used in the proof : conj axiom_04 axiom_45 axiom_18 axiom_46 axiom_47 axiom_40 axiom axiom_61 % 32.81/33.01 %------------------------------------------------------------------------------