%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV161+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:29 EDT 2022 % Result : Theorem 1.37s 1.55s % Output : Refutation 1.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV161+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.13/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 16 05:24:26 EDT 2022 % 0.20/0.35 % CPUTime : % 1.37/1.55 % 1.37/1.55 SPASS V 3.9 % 1.37/1.55 SPASS beiseite: Proof found. % 1.37/1.55 % SZS status Theorem % 1.37/1.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.37/1.55 SPASS derived 4811 clauses, backtracked 267 clauses, performed 4 splits and kept 2589 clauses. % 1.37/1.55 SPASS allocated 89430 KBytes. % 1.37/1.55 SPASS spent 0:00:01.17 on the problem. % 1.37/1.55 0:00:00.04 for the input. % 1.37/1.55 0:00:00.08 for the FLOTTER CNF translation. % 1.37/1.55 0:00:00.04 for inferences. % 1.37/1.55 0:00:00.02 for the backtracking. % 1.37/1.55 0:00:00.87 for the reduction. % 1.37/1.55 % 1.37/1.55 % 1.37/1.55 Here is a proof with depth 5, length 46 : % 1.37/1.55 % SZS output start Refutation % 1.37/1.55 2[0:Inp] || -> leq(n0,skc1)*r. % 1.37/1.55 3[0:Inp] || -> leq(n0,pv10)*r. % 1.37/1.55 5[0:Inp] || -> leq(skc1,pv10)*l. % 1.37/1.55 36[0:Inp] || gt(u,u)* -> . % 1.37/1.55 38[0:Inp] || -> equal(succ(tptp_minus_1),n0)**. % 1.37/1.55 57[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.37/1.55 78[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.37/1.55 80[0:Inp] || leq(u,v)*+ -> gt(succ(v),u)*. % 1.37/1.55 92[0:Inp] || -> equal(sum__dfg(n0,n4,a_select3(q,pv10,tptp_sum_index)),n1)**. % 1.37/1.55 101[0:Inp] || equal(sum__dfg(n0,n4,a_select3(q,skc1,tptp_sum_index)),n1)** -> . % 1.37/1.55 102[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.37/1.55 108[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 1.37/1.55 112[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.37/1.55 116[0:Inp] || leq(u,pred(pv10)) leq(n0,u) -> equal(sum__dfg(n0,n4,a_select3(q,u,tptp_sum_index)),n1)**. % 1.37/1.55 177[0:Res:5.0,102.0] || -> gt(pv10,skc1)*r equal(skc1,pv10). % 1.37/1.55 296[0:Res:3.0,112.0] || leq(pv10,n1)*r -> equal(n1,pv10) equal(pv10,n0). % 1.37/1.55 479[1:Spt:296.2] || -> equal(pv10,n0)**. % 1.37/1.55 608[1:Rew:479.0,92.0] || -> equal(sum__dfg(n0,n4,a_select3(q,n0,tptp_sum_index)),n1)**. % 1.37/1.55 611[1:Rew:479.0,177.0] || -> gt(n0,skc1)*r equal(skc1,pv10). % 1.37/1.55 641[1:Rew:479.0,611.1] || -> gt(n0,skc1)*r equal(skc1,n0). % 1.37/1.55 742[0:SpR:38.0,57.0] || -> equal(pred(n0),tptp_minus_1)**. % 1.37/1.55 2129[2:Spt:641.1] || -> equal(skc1,n0)**. % 1.37/1.55 2135[2:Rew:2129.0,101.0] || equal(sum__dfg(n0,n4,a_select3(q,n0,tptp_sum_index)),n1)** -> . % 1.37/1.55 2175[2:Rew:608.0,2135.0] || equal(n1,n1)* -> . % 1.37/1.55 2176[2:Obv:2175.0] || -> . % 1.37/1.55 2180[2:Spt:2176.0,641.1,2129.0] || equal(skc1,n0)** -> . % 1.37/1.55 2181[2:Spt:2176.0,641.0] || -> gt(n0,skc1)*r. % 1.37/1.55 3501[2:Res:2181.0,78.0] || -> leq(skc1,pred(n0))*r. % 1.37/1.55 3643[2:Rew:742.0,3501.0] || -> leq(skc1,tptp_minus_1)*l. % 1.37/1.55 4364[2:OCh:108.1,108.0,3643.0,2.0] || -> leq(n0,tptp_minus_1)*r. % 1.37/1.55 4382[2:Res:4364.0,80.0] || -> gt(succ(tptp_minus_1),n0)*l. % 1.37/1.55 4393[2:Rew:38.0,4382.0] || -> gt(n0,n0)*. % 1.37/1.55 4394[2:MRR:4393.0,36.0] || -> . % 1.37/1.55 4399[1:Spt:4394.0,296.2,479.0] || equal(pv10,n0)** -> . % 1.37/1.55 4400[1:Spt:4394.0,296.0,296.1] || leq(pv10,n1)*r -> equal(n1,pv10). % 1.37/1.55 4585[2:Spt:177.1] || -> equal(skc1,pv10)**. % 1.37/1.55 4587[2:Rew:4585.0,101.0] || equal(sum__dfg(n0,n4,a_select3(q,pv10,tptp_sum_index)),n1)** -> . % 1.37/1.55 4634[2:Rew:92.0,4587.0] || equal(n1,n1)* -> . % 1.37/1.55 4635[2:Obv:4634.0] || -> . % 1.37/1.55 4639[2:Spt:4635.0,177.1,4585.0] || equal(skc1,pv10)** -> . % 1.37/1.55 4640[2:Spt:4635.0,177.0] || -> gt(pv10,skc1)*r. % 1.37/1.55 4641[2:Res:4640.0,78.0] || -> leq(skc1,pred(pv10))*r. % 1.37/1.55 6466[0:SpL:116.2,101.0] || leq(skc1,pred(pv10))*r leq(n0,skc1) equal(n1,n1) -> . % 1.37/1.55 6467[0:Obv:6466.2] || leq(skc1,pred(pv10))*r leq(n0,skc1) -> . % 1.37/1.55 6468[0:MRR:6467.1,2.0] || leq(skc1,pred(pv10))*r -> . % 1.37/1.55 6469[2:MRR:6468.0,4641.0] || -> . % 1.37/1.55 % SZS output end Refutation % 1.37/1.55 Formulae used in the proof : cl5_nebula_norm_0011 irreflexivity_gt succ_tptp_minus_1 pred_succ leq_gt_pred leq_succ_gt_equiv leq_gt2 transitivity_leq finite_domain_1 % 1.37/1.55 %------------------------------------------------------------------------------