%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV028+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:41:02 EDT 2022 % Result : Theorem 0.19s 0.52s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV028+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/0.13 % Command : run_spass %d %s % 0.12/0.33 % Computer : n016.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 : Wed Jun 15 03:43:17 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.52 % 0.19/0.52 SPASS V 3.9 % 0.19/0.52 SPASS beiseite: Proof found. % 0.19/0.52 % SZS status Theorem % 0.19/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 SPASS derived 6 clauses, backtracked 0 clauses, performed 0 splits and kept 175 clauses. % 0.19/0.52 SPASS allocated 85888 KBytes. % 0.19/0.52 SPASS spent 0:00:00.17 on the problem. % 0.19/0.52 0:00:00.04 for the input. % 0.19/0.52 0:00:00.09 for the FLOTTER CNF translation. % 0.19/0.52 0:00:00.00 for inferences. % 0.19/0.52 0:00:00.00 for the backtracking. % 0.19/0.52 0:00:00.02 for the reduction. % 0.19/0.52 % 0.19/0.52 % 0.19/0.52 Here is a proof with depth 0, length 38 : % 0.19/0.52 % SZS output start Refutation % 0.19/0.52 1[0:Inp] || -> SkC0*. % 0.19/0.52 2[0:Inp] || -> SkC1*. % 0.19/0.52 3[0:Inp] || -> SkC2*. % 0.19/0.52 4[0:Inp] || -> SkC3*. % 0.19/0.52 12[0:Inp] || -> equal(init,s_best7_init)**. % 0.19/0.52 13[0:Inp] || -> equal(init,s_sworst7_init)**. % 0.19/0.52 14[0:Inp] || -> equal(init,s_worst7_init)**. % 0.19/0.52 15[0:Inp] || -> leq(n0,s_best7)*r. % 0.19/0.52 16[0:Inp] || -> leq(n0,s_sworst7)*r. % 0.19/0.52 17[0:Inp] || -> leq(n0,s_worst7)*r. % 0.19/0.52 19[0:Inp] || -> leq(n0,pv1376)*r. % 0.19/0.52 20[0:Inp] || -> leq(s_best7,n3)*r. % 0.19/0.52 21[0:Inp] || -> leq(s_sworst7,n3)*r. % 0.19/0.52 22[0:Inp] || -> leq(s_worst7,n3)*r. % 0.19/0.52 23[0:Inp] || -> leq(pv1376,n3)*r. % 0.19/0.52 85[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1400_init)**. % 0.19/0.52 86[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1401_init)**. % 0.19/0.52 87[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1402_init)**. % 0.19/0.52 171[0:Inp] || equal(init,init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.19/0.52 172[0:Inp] || equal(init,pvar1400_init) equal(init,pvar1401_init) equal(init,pvar1402_init) equal(init,init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> . % 0.19/0.52 173[0:Rew:14.0,13.0] || -> equal(s_worst7_init,s_sworst7_init)**. % 0.19/0.52 174[0:Rew:173.0,14.0] || -> equal(init,s_sworst7_init)**. % 0.19/0.52 175[0:Rew:12.0,174.0] || -> equal(s_sworst7_init,s_best7_init)**. % 0.19/0.52 176[0:Rew:175.0,173.0] || -> equal(s_worst7_init,s_best7_init)**. % 0.19/0.52 191[0:Rew:12.0,87.1] || gt(loopcounter,n1) -> equal(pvar1402_init,s_best7_init)**. % 0.19/0.52 192[0:Rew:12.0,86.1] || gt(loopcounter,n1) -> equal(pvar1401_init,s_best7_init)**. % 0.19/0.52 193[0:Rew:12.0,85.1] || gt(loopcounter,n1) -> equal(pvar1400_init,s_best7_init)**. % 0.19/0.52 202[0:Obv:171.0] || equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.19/0.52 203[0:Rew:12.0,202.2,176.0,202.2,12.0,202.1,175.0,202.1,12.0,202.0] || equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.19/0.52 204[0:Obv:203.2] || leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.19/0.52 205[0:MRR:204.0,204.1,204.2,204.3,204.4,204.5,204.6,204.7,204.8,204.9,204.10,204.11,15.0,16.0,17.0,19.0,20.0,21.0,22.0,23.0,1.0,2.0,3.0,4.0] || -> gt(loopcounter,n1)*l. % 0.19/0.52 206[0:MRR:191.0,205.0] || -> equal(pvar1402_init,s_best7_init)**. % 0.19/0.52 207[0:MRR:192.0,205.0] || -> equal(pvar1401_init,s_best7_init)**. % 0.19/0.52 208[0:MRR:193.0,205.0] || -> equal(pvar1400_init,s_best7_init)**. % 0.19/0.52 209[0:Obv:172.3] || equal(init,pvar1400_init) equal(init,pvar1401_init) equal(init,pvar1402_init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> . % 0.19/0.52 210[0:Rew:12.0,209.5,176.0,209.5,12.0,209.4,175.0,209.4,12.0,209.3,12.0,209.2,206.0,209.2,12.0,209.1,207.0,209.1,12.0,209.0,208.0,209.0] || equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> . % 0.19/0.52 211[0:Obv:210.5] || leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv1376) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv1376,n3) SkC0* SkC1 SkC2 SkC3 -> . % 0.19/0.52 212[0:MRR:211.0,211.1,211.2,211.3,211.4,211.5,211.6,211.7,211.8,211.9,211.10,211.11,15.0,16.0,17.0,19.0,20.0,21.0,22.0,23.0,1.0,2.0,3.0,4.0] || -> . % 0.19/0.52 % SZS output end Refutation % 0.19/0.52 Formulae used in the proof : gauss_init_0025 gt_succ leq_succ_gt_equiv % 0.19/0.52 %------------------------------------------------------------------------------