%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV034+1 : TPTP v8.1.0. Bugfixed v3.3.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:41:03 EDT 2022 % Result : Theorem 0.21s 0.53s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SWV034+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.13/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Thu Jun 16 04:35:08 EDT 2022 % 0.13/0.35 % CPUTime : % 0.21/0.53 % 0.21/0.53 SPASS V 3.9 % 0.21/0.53 SPASS beiseite: Proof found. % 0.21/0.53 % SZS status Theorem % 0.21/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.21/0.53 SPASS derived 6 clauses, backtracked 0 clauses, performed 0 splits and kept 173 clauses. % 0.21/0.53 SPASS allocated 85869 KBytes. % 0.21/0.53 SPASS spent 0:00:00.17 on the problem. % 0.21/0.53 0:00:00.04 for the input. % 0.21/0.53 0:00:00.09 for the FLOTTER CNF translation. % 0.21/0.53 0:00:00.00 for inferences. % 0.21/0.53 0:00:00.00 for the backtracking. % 0.21/0.53 0:00:00.02 for the reduction. % 0.21/0.53 % 0.21/0.53 % 0.21/0.53 Here is a proof with depth 0, length 40 : % 0.21/0.53 % SZS output start Refutation % 0.21/0.53 1[0:Inp] || -> SkC0*. % 0.21/0.53 2[0:Inp] || -> SkC1*. % 0.21/0.53 3[0:Inp] || -> SkC2*. % 0.21/0.53 4[0:Inp] || -> SkC3*. % 0.21/0.53 11[0:Inp] || -> equal(init,s_best7_init)**. % 0.21/0.53 12[0:Inp] || -> equal(init,s_sworst7_init)**. % 0.21/0.53 13[0:Inp] || -> equal(init,s_worst7_init)**. % 0.21/0.53 14[0:Inp] || -> leq(n0,s_best7)*r. % 0.21/0.53 15[0:Inp] || -> leq(n0,s_sworst7)*r. % 0.21/0.53 16[0:Inp] || -> leq(n0,s_worst7)*r. % 0.21/0.53 17[0:Inp] || -> leq(n0,pv19)*r. % 0.21/0.53 18[0:Inp] || -> leq(s_best7,n3)*r. % 0.21/0.53 19[0:Inp] || -> leq(s_sworst7,n3)*r. % 0.21/0.53 20[0:Inp] || -> leq(s_worst7,n3)*r. % 0.21/0.53 55[0:Inp] || -> leq(pv19,minus(n410,n1))*r. % 0.21/0.53 80[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 0.21/0.53 82[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1400_init)**. % 0.21/0.53 83[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1401_init)**. % 0.21/0.53 84[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1402_init)**. % 0.21/0.53 168[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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,minus(n410,n1))*r SkC0 SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.21/0.53 169[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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,minus(n410,n1))*r SkC0 SkC1 SkC2 SkC3 -> . % 0.21/0.53 170[0:Rew:13.0,12.0] || -> equal(s_worst7_init,s_sworst7_init)**. % 0.21/0.53 171[0:Rew:170.0,13.0] || -> equal(init,s_sworst7_init)**. % 0.21/0.53 172[0:Rew:11.0,171.0] || -> equal(s_sworst7_init,s_best7_init)**. % 0.21/0.53 173[0:Rew:172.0,170.0] || -> equal(s_worst7_init,s_best7_init)**. % 0.21/0.53 187[0:Rew:80.0,55.0] || -> leq(pv19,pred(n410))*r. % 0.21/0.53 188[0:Rew:11.0,84.1] || gt(loopcounter,n1) -> equal(pvar1402_init,s_best7_init)**. % 0.21/0.53 189[0:Rew:11.0,83.1] || gt(loopcounter,n1) -> equal(pvar1401_init,s_best7_init)**. % 0.21/0.53 190[0:Rew:11.0,82.1] || gt(loopcounter,n1) -> equal(pvar1400_init,s_best7_init)**. % 0.21/0.53 199[0:Obv:168.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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,minus(n410,n1))*r SkC0 SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.21/0.53 200[0:Rew:80.0,199.10,11.0,199.2,173.0,199.2,11.0,199.1,172.0,199.1,11.0,199.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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,pred(n410))*r SkC0 SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.21/0.53 201[0:Obv:200.2] || leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,pred(n410))*r SkC0 SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 0.21/0.53 202[0:MRR:201.0,201.1,201.2,201.3,201.4,201.5,201.6,201.7,201.8,201.9,201.10,201.11,14.0,15.0,16.0,17.0,18.0,19.0,20.0,187.0,1.0,2.0,3.0,4.0] || -> gt(loopcounter,n1)*l. % 0.21/0.53 203[0:MRR:188.0,202.0] || -> equal(pvar1402_init,s_best7_init)**. % 0.21/0.53 204[0:MRR:189.0,202.0] || -> equal(pvar1401_init,s_best7_init)**. % 0.21/0.53 205[0:MRR:190.0,202.0] || -> equal(pvar1400_init,s_best7_init)**. % 0.21/0.53 206[0:Obv:169.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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,minus(n410,n1))*r SkC0 SkC1 SkC2 SkC3 -> . % 0.21/0.53 207[0:Rew:80.0,206.13,11.0,206.5,173.0,206.5,11.0,206.4,172.0,206.4,11.0,206.3,11.0,206.2,203.0,206.2,11.0,206.1,204.0,206.1,11.0,206.0,205.0,206.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,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,pred(n410))*r SkC0 SkC1 SkC2 SkC3 -> . % 0.21/0.53 208[0:Obv:207.5] || leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(n0,pv19) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) leq(pv19,pred(n410))*r SkC0 SkC1 SkC2 SkC3 -> . % 0.21/0.53 209[0:MRR:208.0,208.1,208.2,208.3,208.4,208.5,208.6,208.7,208.8,208.9,208.10,208.11,14.0,15.0,16.0,17.0,18.0,19.0,20.0,187.0,1.0,2.0,3.0,4.0] || -> . % 0.21/0.53 % SZS output end Refutation % 0.21/0.53 Formulae used in the proof : gauss_init_0049 gt_succ leq_succ_gt_equiv pred_minus_1 % 0.21/0.53 %------------------------------------------------------------------------------