%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM853+1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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 : Mon Jul 18 14:31:06 EDT 2022 % Result : Theorem 0.73s 0.91s % Output : Refutation 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM853+1 : TPTP v8.1.0. Released v4.1.0. % 0.11/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jul 7 15:11:07 EDT 2022 % 0.14/0.34 % CPUTime : % 0.73/0.91 % 0.73/0.91 SPASS V 3.9 % 0.73/0.91 SPASS beiseite: Proof found. % 0.73/0.91 % SZS status Theorem % 0.73/0.91 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.73/0.91 SPASS derived 2521 clauses, backtracked 8 clauses, performed 1 splits and kept 1232 clauses. % 0.73/0.91 SPASS allocated 87230 KBytes. % 0.73/0.91 SPASS spent 0:00:00.55 on the problem. % 0.73/0.91 0:00:00.03 for the input. % 0.73/0.91 0:00:00.03 for the FLOTTER CNF translation. % 0.73/0.91 0:00:00.03 for inferences. % 0.73/0.91 0:00:00.00 for the backtracking. % 0.73/0.91 0:00:00.42 for the reduction. % 0.73/0.91 % 0.73/0.91 % 0.73/0.91 Here is a proof with depth 10, length 28 : % 0.73/0.91 % SZS output start Refutation % 0.73/0.91 2[0:Inp] || greater(vd486,vd488)* -> . % 0.73/0.91 4[0:Inp] || greater(u,u)* -> . % 0.73/0.91 7[0:Inp] || -> greater(vplus(u,v),u)*. % 0.73/0.91 15[0:Inp] || -> greater(vmul(vd486,vd487),vmul(vd488,vd487))*. % 0.73/0.91 25[0:Inp] || less(u,v) -> greater(v,u)*. % 0.73/0.91 27[0:Inp] || -> equal(vplus(u,v),vplus(v,u))*. % 0.73/0.91 32[0:Inp] || -> less(u,v) greater(u,v)* equal(u,v). % 0.73/0.91 44[0:Inp] || greater(u,v) -> greater(vmul(u,w),vmul(v,w))*. % 0.73/0.91 56[0:Inp] || greater(u,v) -> equal(vplus(v,skf5(v,u)),u)**. % 0.73/0.91 58[0:Inp] || -> equal(vplus(vplus(u,v),w),vplus(u,vplus(v,w)))**. % 0.73/0.91 70[0:Res:25.1,2.0] || less(vd488,vd486)*l -> . % 0.73/0.91 71[0:Res:32.1,2.0] || -> less(vd486,vd488)*r equal(vd488,vd486). % 0.73/0.91 75[1:Spt:71.1] || -> equal(vd488,vd486)**. % 0.73/0.91 79[1:Rew:75.0,15.0] || -> greater(vmul(vd486,vd487),vmul(vd486,vd487))*. % 0.73/0.91 81[1:MRR:79.0,4.0] || -> . % 0.73/0.91 82[1:Spt:81.0,71.1,75.0] || equal(vd488,vd486)** -> . % 0.73/0.91 83[1:Spt:81.0,71.0] || -> less(vd486,vd488)*r. % 0.73/0.91 98[0:SpR:27.0,7.0] || -> greater(vplus(u,v),v)*. % 0.73/0.91 402[0:SpR:58.0,98.0] || -> greater(vplus(u,vplus(v,w)),w)*. % 0.73/0.91 450[0:SpR:27.0,402.0] || -> greater(vplus(u,vplus(v,w)),v)*. % 0.73/0.91 476[0:SpR:56.1,450.0] || greater(u,v) -> greater(vplus(w,u),v)*. % 0.73/0.91 2575[0:Res:476.1,4.0] || greater(u,vplus(v,u))* -> . % 0.73/0.91 2649[0:SpL:27.0,2575.0] || greater(u,vplus(u,v))* -> . % 0.73/0.91 2680[0:SpL:56.1,2649.0] || greater(u,v)*+ greater(v,u)* -> . % 0.73/0.91 3071[0:Res:15.0,2680.0] || greater(vmul(vd488,vd487),vmul(vd486,vd487))* -> . % 0.73/0.91 3096[0:Res:44.1,3071.0] || greater(vd488,vd486)* -> . % 0.73/0.91 3099[0:Res:32.1,3096.0] || -> less(vd488,vd486)*l equal(vd488,vd486). % 0.73/0.91 3101[1:MRR:3099.0,3099.1,70.0,82.0] || -> . % 0.73/0.91 % SZS output end Refutation % 0.73/0.91 Formulae used in the proof : holds_a40_conseq_a40_307_a41__a44__a32_490_a44__a32_0_a41_ ass_a40_cond_a40_goal_a40_130_a41__a44__a32_0_a41__a44__a32_3_a41_ ass_a40_cond_a40_189_a44__a32_0_a41__a44__a32_0_a41_ holds_a40_antec_a40_307_a41__a44__a32_489_a44__a32_0_a41_ ass_a40_cond_a40_147_a44__a32_0_a41__a44__a32_0_a41_ ass_a40_cond_a40_61_a44__a32_0_a41__a44__a32_0_a41_ ass_a40_cond_a40_goal_a40_130_a41__a44__a32_0_a41__a44__a32_0_a41_ ass_a40_cond_a40_299_a44__a32_0_a41__a44__a32_2_a41_ def_a40_cond_a40_conseq_a40_axiom_a40_3_a41__a41__a44__a32_11_a41__a44__a32_1_a41_ ass_a40_cond_a40_33_a44__a32_0_a41__a44__a32_0_a41_ % 0.73/0.91 %------------------------------------------------------------------------------