%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV031+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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 5.92s 6.11s % Output : Refutation 5.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV031+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.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 : Thu Jun 16 03:08:42 EDT 2022 % 0.12/0.34 % CPUTime : % 5.92/6.11 % 5.92/6.11 SPASS V 3.9 % 5.92/6.11 SPASS beiseite: Proof found. % 5.92/6.11 % SZS status Theorem % 5.92/6.11 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.92/6.11 SPASS derived 8071 clauses, backtracked 255 clauses, performed 3 splits and kept 4828 clauses. % 5.92/6.11 SPASS allocated 93762 KBytes. % 5.92/6.11 SPASS spent 0:00:05.71 on the problem. % 5.92/6.11 0:00:00.04 for the input. % 5.92/6.11 0:00:00.08 for the FLOTTER CNF translation. % 5.92/6.11 0:00:00.07 for inferences. % 5.92/6.11 0:00:00.08 for the backtracking. % 5.92/6.11 0:00:05.30 for the reduction. % 5.92/6.11 % 5.92/6.11 % 5.92/6.11 Here is a proof with depth 2, length 29 : % 5.92/6.11 % SZS output start Refutation % 5.92/6.11 1[0:Inp] || -> SkC0*. % 5.92/6.11 5[0:Inp] || -> leq(n0,skc3)*r. % 5.92/6.11 7[0:Inp] || -> leq(n0,pv9)*r. % 5.92/6.11 8[0:Inp] || -> leq(n0,pv10)*r. % 5.92/6.11 51[0:Inp] || -> leq(pv9,minus(n410,n1))*r. % 5.92/6.11 52[0:Inp] || -> leq(pv10,minus(n330,n1))*r. % 5.92/6.11 77[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 5.92/6.11 120[0:Inp] || leq(u,n3) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 5.92/6.11 140[0:Inp] || leq(u,v) leq(w,u) leq(x,y) leq(y,z) -> equal(a_select3(tptp_const_array2(dim(x,z),dim(w,v),x1),y,u),x1)**. % 5.92/6.11 148[0:Inp] || equal(init,init) equal(a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,minus(n410,n1)) SkC0 -> leq(skc3,n3). % 5.92/6.11 153[0:Inp] || equal(a_select2(s_values7_init,skc3),init) equal(init,init) equal(a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,minus(n410,n1)) SkC0 -> . % 5.92/6.11 175[0:Rew:77.0,52.0] || -> leq(pv10,pred(n330))*r. % 5.92/6.11 176[0:Rew:77.0,51.0] || -> leq(pv9,pred(n410))*r. % 5.92/6.11 178[0:Obv:153.1] || equal(a_select2(s_values7_init,skc3),init) equal(a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,minus(n410,n1)) SkC0 -> . % 5.92/6.11 179[0:Rew:77.0,178.3,77.0,178.1,77.0,178.1] || equal(a_select2(s_values7_init,skc3),init) equal(a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,pred(n410)) SkC0 -> . % 5.92/6.11 180[0:MRR:179.2,179.3,179.4,7.0,176.0,1.0] || equal(a_select2(s_values7_init,skc3),init) equal(a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10),init)** -> . % 5.92/6.11 181[0:Obv:148.0] || equal(a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,minus(n410,n1)) SkC0 -> leq(skc3,n3). % 5.92/6.11 182[0:Rew:77.0,181.2,77.0,181.0,77.0,181.0] || equal(a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10),init)** leq(n0,pv9) leq(pv9,pred(n410)) SkC0 -> leq(skc3,n3). % 5.92/6.11 183[0:MRR:182.1,182.2,182.3,7.0,176.0,1.0] || equal(a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10),init)** -> leq(skc3,n3). % 5.92/6.11 10742[0:SpL:140.4,180.1] || leq(pv10,pred(n330)) leq(n0,pv10) leq(n0,pv9) leq(pv9,pred(n410)) equal(a_select2(s_values7_init,skc3),init)** equal(init,init) -> . % 5.92/6.11 10743[0:Obv:10742.5] || leq(pv10,pred(n330)) leq(n0,pv10) leq(n0,pv9) leq(pv9,pred(n410)) equal(a_select2(s_values7_init,skc3),init)** -> . % 5.92/6.11 10744[0:MRR:10743.0,10743.1,10743.2,10743.3,175.0,8.0,7.0,176.0] || equal(a_select2(s_values7_init,skc3),init)** -> . % 5.92/6.11 10745[0:SpL:120.2,10744.0] || leq(skc3,n3) leq(n0,skc3) equal(init,init)* -> . % 5.92/6.11 10746[0:Obv:10745.2] || leq(skc3,n3)*l leq(n0,skc3) -> . % 5.92/6.11 10747[0:MRR:10746.1,5.0] || leq(skc3,n3)*l -> . % 5.92/6.11 10748[0:MRR:183.1,10747.0] || equal(a_select3(tptp_const_array2(dim(n0,pred(n410)),dim(n0,pred(n330)),init),pv9,pv10),init)** -> . % 5.92/6.11 10799[0:SpL:140.4,10748.0] || leq(pv10,pred(n330))*r leq(n0,pv10) leq(n0,pv9) leq(pv9,pred(n410)) equal(init,init) -> . % 5.92/6.11 10800[0:Obv:10799.4] || leq(pv10,pred(n330))*r leq(n0,pv10) leq(n0,pv9) leq(pv9,pred(n410)) -> . % 5.92/6.11 10801[0:MRR:10800.0,10800.1,10800.2,10800.3,175.0,8.0,7.0,176.0] || -> . % 5.92/6.11 % SZS output end Refutation % 5.92/6.11 Formulae used in the proof : gauss_init_0037 gt_succ leq_succ_gt_equiv pred_minus_1 const_array2_select % 5.92/6.11 %------------------------------------------------------------------------------