%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HEN008-2 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n012.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 : Sat Jul 16 13:03:08 EDT 2022 % Result : Unsatisfiable 14.65s 14.83s % Output : Refutation 14.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : HEN008-2 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n012.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Fri Jul 1 13:11:17 EDT 2022 % 0.13/0.34 % CPUTime : % 14.65/14.83 % 14.65/14.83 SPASS V 3.9 % 14.65/14.83 SPASS beiseite: Proof found. % 14.65/14.83 % SZS status Theorem % 14.65/14.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 14.65/14.83 SPASS derived 37177 clauses, backtracked 0 clauses, performed 0 splits and kept 6204 clauses. % 14.65/14.83 SPASS allocated 92577 KBytes. % 14.65/14.83 SPASS spent 0:0:13.43 on the problem. % 14.65/14.83 0:00:00.04 for the input. % 14.65/14.83 0:00:00.00 for the FLOTTER CNF translation. % 14.65/14.83 0:00:00.39 for inferences. % 14.65/14.83 0:00:00.00 for the backtracking. % 14.65/14.83 0:0:12.93 for the reduction. % 14.65/14.83 % 14.65/14.83 % 14.65/14.83 Here is a proof with depth 5, length 31 : % 14.65/14.83 % SZS output start Refutation % 14.65/14.83 2[0:Inp] || -> quotient(zero,u,zero)*. % 14.65/14.83 3[0:Inp] || -> quotient(u,u,zero)*. % 14.65/14.83 4[0:Inp] || -> quotient(u,zero,u)*. % 14.65/14.83 5[0:Inp] || less_equal(u,v)* less_equal(v,w)* -> less_equal(u,w)*. % 14.65/14.83 6[0:Inp] || less_equal(u,v)*+ quotient(w,v,x)* quotient(w,y,u)* -> less_equal(x,y)*. % 14.65/14.83 7[0:Inp] || less_equal(u,v)*+ quotient(w,u,x)* quotient(w,v,y)* -> less_equal(y,x)*. % 14.65/14.83 8[0:Inp] || -> less_equal(a,b)*r. % 14.65/14.83 9[0:Inp] || -> quotient(a,c,aQc)*. % 14.65/14.83 10[0:Inp] || -> quotient(b,c,bQc)*. % 14.65/14.83 11[0:Inp] || less_equal(aQc,bQc)*r -> . % 14.65/14.83 15[0:Inp] || quotient(u,v,w)*+ quotient(x,y,z)* quotient(x1,v,x)* quotient(x2,v,y)* quotient(x1,x2,u)* -> less_equal(z,w)*. % 14.65/14.83 16[0:Inp] || -> less_equal(zero,u)*. % 14.65/14.83 17[0:Inp] || less_equal(u,v)*+ less_equal(v,u)* -> equal(v,u). % 14.65/14.83 19[0:Inp] || -> quotient(u,v,divide(u,v))*. % 14.65/14.83 23[0:Res:6.3,11.0] || less_equal(u,v)*+ quotient(w,v,aQc)* quotient(w,bQc,u)* -> . % 14.65/14.83 71[0:Res:16.0,17.0] || less_equal(u,zero)* -> equal(u,zero). % 14.65/14.83 105[0:Res:8.0,7.0] || quotient(u,a,v)*+ quotient(u,b,w)* -> less_equal(w,v)*. % 14.65/14.83 194[0:Res:2.0,15.0] || quotient(u,v,w)*+ quotient(x,y,u)* quotient(z,y,v)* quotient(x,z,zero)* -> less_equal(w,zero). % 14.65/14.83 553[0:Res:3.0,105.0] || quotient(a,b,u)* -> less_equal(u,zero). % 14.65/14.83 794[0:Res:19.0,553.0] || -> less_equal(divide(a,b),zero)*l. % 14.65/14.83 807[0:Res:794.0,71.0] || -> equal(divide(a,b),zero)**. % 14.65/14.83 845[0:SpR:807.0,19.0] || -> quotient(a,b,zero)*. % 14.65/14.83 886[0:NCh:5.2,5.1,23.0,16.0] || equal(u,zero) quotient(v,w,aQc)*+ quotient(v,bQc,u)* -> . % 14.65/14.83 2078[0:Res:19.0,194.0] || quotient(u,v,w)*+ quotient(x,v,y)* quotient(u,x,zero)* -> less_equal(divide(w,y),zero)*l. % 14.65/14.83 2090[0:Res:4.0,886.1] || equal(u,zero) quotient(aQc,bQc,u)* -> . % 14.65/14.83 2142[0:Res:19.0,2090.1] || equal(divide(aQc,bQc),zero)** -> . % 14.65/14.83 19095[0:Res:9.0,2078.0] || quotient(u,c,v)*+ quotient(a,u,zero)* -> less_equal(divide(aQc,v),zero). % 14.65/14.83 48863[0:Res:10.0,19095.0] || quotient(a,b,zero)* -> less_equal(divide(aQc,bQc),zero). % 14.65/14.83 48884[0:MRR:48863.0,845.0] || -> less_equal(divide(aQc,bQc),zero)*l. % 14.65/14.83 48926[0:Res:48884.0,71.0] || -> equal(divide(aQc,bQc),zero)**. % 14.65/14.83 49027[0:MRR:48926.0,2142.0] || -> . % 14.65/14.83 % SZS output end Refutation % 14.65/14.83 Formulae used in the proof : zero_divide_anything_is_zero x_divide_x_is_zero x_divde_zero_is_x transitivity_of_less_equal xQyLEz_implies_xQzLEy xLEy_implies_zQyLEzQx aLEb aQc bQc prove_aQcLEbQc quotient_property zero_is_smallest less_equal_and_equal closure % 14.65/14.83 %------------------------------------------------------------------------------