%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HEN009-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:10 EDT 2022 % Result : Unsatisfiable 32.52s 32.69s % Output : Refutation 32.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : HEN009-2 : TPTP v8.1.0. Released v1.0.0. % 0.11/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 14:25:17 EDT 2022 % 0.13/0.34 % CPUTime : % 32.52/32.69 % 32.52/32.69 SPASS V 3.9 % 32.52/32.69 SPASS beiseite: Proof found. % 32.52/32.69 % SZS status Theorem % 32.52/32.69 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 32.52/32.69 SPASS derived 55893 clauses, backtracked 0 clauses, performed 0 splits and kept 7528 clauses. % 32.52/32.69 SPASS allocated 106772 KBytes. % 32.52/32.69 SPASS spent 0:0:29.19 on the problem. % 32.52/32.69 0:00:00.04 for the input. % 32.52/32.69 0:00:00.00 for the FLOTTER CNF translation. % 32.52/32.69 0:00:00.57 for inferences. % 32.52/32.69 0:00:00.00 for the backtracking. % 32.52/32.69 0:0:28.48 for the reduction. % 32.52/32.69 % 32.52/32.69 % 32.52/32.69 Here is a proof with depth 9, length 53 : % 32.52/32.69 % SZS output start Refutation % 32.52/32.69 3[0:Inp] || -> quotient(u,u,zero)*. % 32.52/32.69 4[0:Inp] || -> quotient(u,zero,u)*. % 32.52/32.69 6[0:Inp] || less_equal(u,v)*+ quotient(w,v,x)* quotient(w,y,u)* -> less_equal(x,y)*. % 32.52/32.69 7[0:Inp] || less_equal(u,v)*+ quotient(w,u,x)* quotient(w,v,y)* -> less_equal(y,x)*. % 32.52/32.69 8[0:Inp] || less_equal(u,v)*+ quotient(v,w,x)* quotient(u,w,y)* -> less_equal(y,x)*. % 32.52/32.69 9[0:Inp] || -> quotient(identity,a,idQa)*. % 32.52/32.69 10[0:Inp] || -> quotient(identity,idQa,idQ_idQa)*. % 32.52/32.69 11[0:Inp] || -> quotient(identity,idQ_idQa,idQ__idQ_idQa)*. % 32.52/32.69 12[0:Inp] || equal(idQ__idQ_idQa,idQa)** -> . % 32.52/32.69 14[0:Inp] || quotient(u,v,zero)* -> less_equal(u,v). % 32.52/32.69 15[0:Inp] || quotient(u,v,w)* -> less_equal(w,u). % 32.52/32.69 16[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)*. % 32.52/32.69 17[0:Inp] || -> less_equal(zero,u)*. % 32.52/32.69 18[0:Inp] || less_equal(u,v)*+ less_equal(v,u)* -> equal(v,u). % 32.52/32.69 19[0:Inp] || -> less_equal(u,identity)*. % 32.52/32.69 20[0:Inp] || -> quotient(u,v,divide(u,v))*. % 32.52/32.69 21[0:Inp] || quotient(u,v,w)*+ quotient(u,v,x)* -> equal(x,w)*. % 32.52/32.69 23[0:Res:18.2,12.0] || less_equal(idQa,idQ__idQ_idQa) less_equal(idQ__idQ_idQa,idQa)*l -> . % 32.52/32.69 31[0:Res:3.0,14.0] || -> less_equal(u,u)*. % 32.52/32.69 41[0:Res:20.0,15.0] || -> less_equal(divide(u,v),u)*l. % 32.52/32.69 44[0:Res:11.0,21.0] || quotient(identity,idQ_idQa,u)* -> equal(u,idQ__idQ_idQa). % 32.52/32.69 49[0:Res:3.0,21.0] || quotient(u,u,v)* -> equal(v,zero). % 32.52/32.69 50[0:Res:4.0,21.0] || quotient(u,zero,v)* -> equal(v,u). % 32.52/32.69 54[0:Res:20.0,44.0] || -> equal(divide(identity,idQ_idQa),idQ__idQ_idQa)**. % 32.52/32.69 65[0:Res:17.0,18.0] || less_equal(u,zero)* -> equal(u,zero). % 32.52/32.69 98[0:Res:19.0,8.0] || quotient(identity,u,v)*+ quotient(w,u,x)* -> less_equal(x,v)*. % 32.52/32.69 125[0:Res:20.0,49.0] || -> equal(divide(u,u),zero)**. % 32.52/32.69 133[0:Res:41.0,7.0] || quotient(u,divide(v,w),x)*+ quotient(u,v,y)* -> less_equal(y,x)*. % 32.52/32.69 151[0:Res:20.0,50.0] || -> equal(divide(u,zero),u)**. % 32.52/32.69 175[0:Res:31.0,6.0] || quotient(u,v,w)*+ quotient(u,x,v)* -> less_equal(w,x)*. % 32.52/32.69 217[0:Res:20.0,16.0] || quotient(u,v,w)*+ quotient(x,y,u)* quotient(z,y,v)* quotient(x,z,x1)* -> less_equal(w,divide(x1,y))*. % 32.52/32.69 498[0:Res:10.0,98.0] || quotient(u,idQa,v)* -> less_equal(v,idQ_idQa). % 32.52/32.69 694[0:Res:20.0,498.0] || -> less_equal(divide(u,idQa),idQ_idQa)*l. % 32.52/32.69 719[0:Res:694.0,18.0] || less_equal(idQ_idQa,divide(u,idQa))*r -> equal(divide(u,idQa),idQ_idQa). % 32.52/32.69 3375[0:Res:20.0,217.0] || quotient(u,v,w)*+ quotient(x,v,y)* quotient(u,x,z)* -> less_equal(divide(w,y),divide(z,v))*. % 32.52/32.69 6114[0:Res:11.0,175.0] || quotient(identity,u,idQ_idQa)* -> less_equal(idQ__idQ_idQa,u). % 32.52/32.69 6121[0:Res:20.0,175.0] || quotient(u,v,w)* -> less_equal(divide(u,w),v). % 32.52/32.69 6138[0:Res:10.0,6114.0] || -> less_equal(idQ__idQ_idQa,idQa)*l. % 32.52/32.69 6143[0:MRR:23.1,6138.0] || less_equal(idQa,idQ__idQ_idQa)*r -> . % 32.52/32.69 6666[0:Res:20.0,6121.0] || -> less_equal(divide(u,divide(u,v)),v)*l. % 32.52/32.69 8296[0:Res:20.0,133.0] || quotient(u,v,w)*+ -> less_equal(w,divide(u,divide(v,x)))*. % 32.52/32.69 14513[0:Res:10.0,3375.0] || quotient(u,idQa,v)*+ quotient(identity,u,w)* -> less_equal(divide(idQ_idQa,v),divide(w,idQa))*. % 32.52/32.69 17326[0:Res:9.0,8296.0] || -> less_equal(idQa,divide(identity,divide(a,u)))*r. % 32.52/32.69 30932[0:Res:20.0,14513.0] || quotient(identity,u,v)*+ -> less_equal(divide(idQ_idQa,divide(u,idQa)),divide(v,idQa))*. % 32.52/32.69 77489[0:Res:9.0,30932.0] || -> less_equal(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa))*l. % 32.52/32.69 77522[0:Rew:125.0,77489.0] || -> less_equal(divide(idQ_idQa,divide(a,idQa)),zero)*l. % 32.52/32.69 77599[0:Res:77522.0,65.0] || -> equal(divide(idQ_idQa,divide(a,idQa)),zero)**. % 32.52/32.69 77835[0:SpR:77599.0,6666.0] || -> less_equal(divide(idQ_idQa,zero),divide(a,idQa))*l. % 32.52/32.69 78134[0:Rew:151.0,77835.0] || -> less_equal(idQ_idQa,divide(a,idQa))*r. % 32.52/32.69 79371[0:Res:78134.0,719.0] || -> equal(divide(a,idQa),idQ_idQa)**. % 32.52/32.69 80067[0:SpR:79371.0,17326.0] || -> less_equal(idQa,divide(identity,idQ_idQa))*r. % 32.52/32.69 80329[0:Rew:54.0,80067.0] || -> less_equal(idQa,idQ__idQ_idQa)*r. % 32.52/32.69 80330[0:MRR:80329.0,6143.0] || -> . % 32.52/32.69 % SZS output end Refutation % 32.52/32.69 Formulae used in the proof : x_divide_x_is_zero x_divde_zero_is_x xQyLEz_implies_xQzLEy xLEy_implies_zQyLEzQx xLEy_implies_xQzLEyQz identity_divide_a identity_divide_idQa identity_divide_idQ_idQa prove_one_inversion_equals_three less_equal_quotient divisor_existence quotient_property zero_is_smallest less_equal_and_equal identity_is_largest closure well_defined % 32.52/32.69 %------------------------------------------------------------------------------