%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV050+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:06 EDT 2022 % Result : Theorem 0.19s 0.51s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV050+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.12/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n011.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 : Tue Jun 14 17:32:19 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.51 % 0.19/0.51 SPASS V 3.9 % 0.19/0.51 SPASS beiseite: Proof found. % 0.19/0.51 % SZS status Theorem % 0.19/0.51 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.51 SPASS derived 39 clauses, backtracked 11 clauses, performed 1 splits and kept 169 clauses. % 0.19/0.51 SPASS allocated 85775 KBytes. % 0.19/0.51 SPASS spent 0:00:00.17 on the problem. % 0.19/0.51 0:00:00.04 for the input. % 0.19/0.51 0:00:00.08 for the FLOTTER CNF translation. % 0.19/0.51 0:00:00.00 for inferences. % 0.19/0.51 0:00:00.00 for the backtracking. % 0.19/0.51 0:00:00.02 for the reduction. % 0.19/0.51 % 0.19/0.51 % 0.19/0.51 Here is a proof with depth 1, length 21 : % 0.19/0.51 % SZS output start Refutation % 0.19/0.51 23[0:Inp] || -> leq(u,u)*. % 0.19/0.51 27[0:Inp] || -> equal(succ(tptp_minus_1),n0)**. % 0.19/0.51 46[0:Inp] || -> equal(pred(succ(u)),u)**. % 0.19/0.51 49[0:Inp] || -> equal(sum__dfg(n0,tptp_minus_1,u),n0)**. % 0.19/0.51 50[0:Inp] || -> equal(sum__dfg(n0,tptp_minus_1,u),tptp_float_0_0)**. % 0.19/0.51 53[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 0.19/0.51 93[0:Inp] || leq(u,n0)* leq(n0,u)* -> equal(u,n0). % 0.19/0.51 110[0:Inp] || -> equal(sum__dfg(n0,minus(n5,n1),divide(abs(minus(a_select2(rho,pv89),a_select2(rhoold,pv89))),plus(abs(a_select2(rho,pv89)),abs(a_select2(rhoold,pv89))))),pv88)**. % 0.19/0.51 111[0:Inp] || -> equal(sum__dfg(n0,minus(n5,n1),divide(abs(minus(a_select2(mu,pv87),a_select2(muold,pv87))),plus(abs(a_select2(mu,pv87)),abs(a_select2(muold,pv87))))),pv86)**. % 0.19/0.51 136[0:Inp] || equal(sum__dfg(n0,minus(n0,n1),divide(abs(minus(a_select2(sigma,pv91),a_select2(sigmaold,pv91))),plus(abs(a_select2(sigma,pv91)),abs(a_select2(sigmaold,pv91))))),n0) equal(sum__dfg(n0,minus(n5,n1),divide(abs(minus(a_select2(mu,pv87),a_select2(muold,pv87))),plus(abs(a_select2(mu,pv87)),abs(a_select2(muold,pv87))))),pv86) equal(sum__dfg(n0,minus(n5,n1),divide(abs(minus(a_select2(rho,pv89),a_select2(rhoold,pv89))),plus(abs(a_select2(rho,pv89)),abs(a_select2(rhoold,pv89))))),pv88)** -> . % 0.19/0.51 138[0:Rew:50.0,49.0] || -> equal(tptp_float_0_0,n0)**. % 0.19/0.51 139[0:Rew:138.0,50.0] || -> equal(sum__dfg(n0,tptp_minus_1,u),n0)**. % 0.19/0.51 150[0:Rew:53.0,110.0] || -> equal(sum__dfg(n0,pred(n5),divide(abs(minus(a_select2(rho,pv89),a_select2(rhoold,pv89))),plus(abs(a_select2(rho,pv89)),abs(a_select2(rhoold,pv89))))),pv88)**. % 0.19/0.51 151[0:Rew:53.0,111.0] || -> equal(sum__dfg(n0,pred(n5),divide(abs(minus(a_select2(mu,pv87),a_select2(muold,pv87))),plus(abs(a_select2(mu,pv87)),abs(a_select2(muold,pv87))))),pv86)**. % 0.19/0.51 152[0:Rew:150.0,136.2,53.0,136.2,151.0,136.1,53.0,136.1,53.0,136.0] || equal(sum__dfg(n0,pred(n0),divide(abs(minus(a_select2(sigma,pv91),a_select2(sigmaold,pv91))),plus(abs(a_select2(sigma,pv91)),abs(a_select2(sigmaold,pv91))))),n0)** equal(pv86,pv86) equal(pv88,pv88) -> . % 0.19/0.51 153[0:Obv:152.2] || equal(sum__dfg(n0,pred(n0),divide(abs(minus(a_select2(sigma,pv91),a_select2(sigmaold,pv91))),plus(abs(a_select2(sigma,pv91)),abs(a_select2(sigmaold,pv91))))),n0)** -> . % 0.19/0.51 159[0:Res:93.2,153.0] || leq(n0,sum__dfg(n0,pred(n0),divide(abs(minus(a_select2(sigma,pv91),a_select2(sigmaold,pv91))),plus(abs(a_select2(sigma,pv91)),abs(a_select2(sigmaold,pv91)))))) leq(sum__dfg(n0,pred(n0),divide(abs(minus(a_select2(sigma,pv91),a_select2(sigmaold,pv91))),plus(abs(a_select2(sigma,pv91)),abs(a_select2(sigmaold,pv91))))),n0)*l -> . % 0.19/0.51 190[0:SpR:27.0,46.0] || -> equal(pred(n0),tptp_minus_1)**. % 0.19/0.51 214[0:Rew:139.0,159.1,190.0,159.1,139.0,159.0,190.0,159.0] || leq(n0,n0)* leq(n0,n0)* -> . % 0.19/0.51 215[0:Obv:214.0] || leq(n0,n0)* -> . % 0.19/0.51 216[0:MRR:215.0,23.0] || -> . % 0.19/0.51 % SZS output end Refutation % 0.19/0.51 Formulae used in the proof : reflexivity_leq succ_tptp_minus_1 pred_succ sum_plus_base sum_plus_base_float pred_minus_1 finite_domain_0 cl5_nebula_norm_0022 % 0.19/0.51 %------------------------------------------------------------------------------