%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV030+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.54s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV030+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.12 % 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 04:59:17 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.54 % 0.19/0.54 SPASS V 3.9 % 0.19/0.54 SPASS beiseite: Proof found. % 0.19/0.54 % SZS status Theorem % 0.19/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.54 SPASS derived 184 clauses, backtracked 0 clauses, performed 0 splits and kept 186 clauses. % 0.19/0.54 SPASS allocated 85869 KBytes. % 0.19/0.54 SPASS spent 0:00:00.19 on the problem. % 0.19/0.54 0:00:00.04 for the input. % 0.19/0.54 0:00:00.09 for the FLOTTER CNF translation. % 0.19/0.54 0:00:00.00 for inferences. % 0.19/0.54 0:00:00.00 for the backtracking. % 0.19/0.54 0:00:00.02 for the reduction. % 0.19/0.54 % 0.19/0.54 % 0.19/0.54 Here is a proof with depth 1, length 26 : % 0.19/0.54 % SZS output start Refutation % 0.19/0.54 1[0:Inp] || -> SkC0*. % 0.19/0.54 5[0:Inp] || -> leq(n0,skc3)*r. % 0.19/0.54 7[0:Inp] || -> leq(n0,pv7)*r. % 0.19/0.54 8[0:Inp] || -> leq(n0,pv19)*r. % 0.19/0.54 9[0:Inp] || -> leq(n0,pv20)*r. % 0.19/0.54 10[0:Inp] || -> leq(n0,pv1376)*r. % 0.19/0.54 11[0:Inp] || -> leq(pv1376,n3)*r. % 0.19/0.54 54[0:Inp] || -> leq(pv7,minus(n410,n1))*r. % 0.19/0.54 55[0:Inp] || -> leq(pv19,minus(n410,n1))*r. % 0.19/0.54 56[0:Inp] || -> leq(pv20,minus(n330,n1))*r. % 0.19/0.54 81[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 0.19/0.54 128[0:Inp] || leq(n0,u) leq(u,minus(pv1376,n1)) -> equal(a_select2(s_values7_init,u),init)**. % 0.19/0.54 161[0:Inp] || equal(init,init) leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,minus(n410,n1)) leq(pv19,minus(n410,n1)) leq(pv20,minus(n330,n1))*r leq(pv1376,n3) SkC0 -> leq(skc3,minus(pv1376,n1)). % 0.19/0.54 162[0:Inp] || equal(a_select2(s_values7_init,skc3),init)** equal(init,init) leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,minus(n410,n1)) leq(pv19,minus(n410,n1)) leq(pv20,minus(n330,n1)) leq(pv1376,n3) SkC0 -> . % 0.19/0.54 179[0:Rew:81.0,56.0] || -> leq(pv20,pred(n330))*r. % 0.19/0.54 180[0:Rew:81.0,55.0] || -> leq(pv19,pred(n410))*r. % 0.19/0.54 181[0:Rew:81.0,54.0] || -> leq(pv7,pred(n410))*r. % 0.19/0.54 182[0:Rew:81.0,128.1] || leq(u,pred(pv1376)) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 0.19/0.54 184[0:Obv:162.1] || equal(a_select2(s_values7_init,skc3),init)** leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,minus(n410,n1)) leq(pv19,minus(n410,n1)) leq(pv20,minus(n330,n1)) leq(pv1376,n3) SkC0 -> . % 0.19/0.54 185[0:Rew:81.0,184.7,81.0,184.6,81.0,184.5] || equal(a_select2(s_values7_init,skc3),init)** leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,pred(n410)) leq(pv19,pred(n410)) leq(pv20,pred(n330)) leq(pv1376,n3) SkC0 -> . % 0.19/0.54 186[0:MRR:185.1,185.2,185.3,185.4,185.5,185.6,185.7,185.8,185.9,7.0,8.0,9.0,10.0,181.0,180.0,179.0,11.0,1.0] || equal(a_select2(s_values7_init,skc3),init)** -> . % 0.19/0.54 187[0:Obv:161.0] || leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,minus(n410,n1)) leq(pv19,minus(n410,n1)) leq(pv20,minus(n330,n1))*r leq(pv1376,n3) SkC0 -> leq(skc3,minus(pv1376,n1)). % 0.19/0.54 188[0:Rew:81.0,187.9,81.0,187.6,81.0,187.5,81.0,187.4] || leq(n0,pv7) leq(n0,pv19) leq(n0,pv20) leq(n0,pv1376) leq(pv7,pred(n410)) leq(pv19,pred(n410)) leq(pv20,pred(n330))*r leq(pv1376,n3) SkC0 -> leq(skc3,pred(pv1376)). % 0.19/0.54 189[0:MRR:188.0,188.1,188.2,188.3,188.4,188.5,188.6,188.7,188.8,7.0,8.0,9.0,10.0,181.0,180.0,179.0,11.0,1.0] || -> leq(skc3,pred(pv1376))*r. % 0.19/0.54 190[0:Res:182.2,186.0] || leq(n0,skc3) leq(skc3,pred(pv1376))*r -> . % 0.19/0.54 379[0:MRR:190.0,190.1,5.0,189.0] || -> . % 0.19/0.54 % SZS output end Refutation % 0.19/0.54 Formulae used in the proof : gauss_init_0033 gt_succ leq_succ_gt_equiv pred_minus_1 % 0.19/0.54 %------------------------------------------------------------------------------