%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HEN007-6 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:07 EDT 2022 % Result : Unsatisfiable 14.12s 14.35s % Output : Refutation 14.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : HEN007-6 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n019.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 : Fri Jul 1 14:48:53 EDT 2022 % 0.13/0.34 % CPUTime : % 14.12/14.35 % 14.12/14.35 SPASS V 3.9 % 14.12/14.35 SPASS beiseite: Proof found. % 14.12/14.35 % SZS status Theorem % 14.12/14.35 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 14.12/14.35 SPASS derived 26504 clauses, backtracked 0 clauses, performed 0 splits and kept 5863 clauses. % 14.12/14.35 SPASS allocated 86698 KBytes. % 14.12/14.35 SPASS spent 0:0:13.47 on the problem. % 14.12/14.35 0:00:00.04 for the input. % 14.12/14.35 0:00:00.00 for the FLOTTER CNF translation. % 14.12/14.35 0:00:00.35 for inferences. % 14.12/14.35 0:00:00.00 for the backtracking. % 14.12/14.35 0:0:13.02 for the reduction. % 14.12/14.35 % 14.12/14.35 % 14.12/14.35 Here is a proof with depth 7, length 26 : % 14.12/14.35 % SZS output start Refutation % 14.12/14.35 4[0:Inp] || -> quotient(u,zero,u)*. % 14.12/14.35 5[0:Inp] || less_equal(u,v)* less_equal(v,w)* -> less_equal(u,w)*. % 14.12/14.35 6[0:Inp] || -> less_equal(x__dfg,y__dfg)*r. % 14.12/14.35 7[0:Inp] || -> quotient(z__dfg,y__dfg,zQy)*. % 14.12/14.35 8[0:Inp] || -> quotient(z__dfg,x__dfg,zQx)*. % 14.12/14.35 9[0:Inp] || less_equal(zQy,zQx)*r -> . % 14.12/14.35 10[0:Inp] || less_equal(u,v) -> quotient(u,v,zero)*. % 14.12/14.35 12[0:Inp] || quotient(u,v,w)* -> less_equal(w,u). % 14.12/14.35 13[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.12/14.35 17[0:Inp] || -> quotient(u,v,divide(u,v))*. % 14.12/14.35 18[0:Inp] || quotient(u,v,w)*+ quotient(u,v,x)* -> equal(x,w)*. % 14.12/14.35 40[0:Res:17.0,12.0] || -> less_equal(divide(u,v),u)*l. % 14.12/14.35 51[0:Res:4.0,18.0] || quotient(u,zero,v)* -> equal(v,u). % 14.12/14.35 52[0:Res:17.0,18.0] || quotient(u,v,w)* -> equal(w,divide(u,v)). % 14.12/14.35 107[0:Res:17.0,13.0] || quotient(u,v,w)*+ quotient(x,y,u)* quotient(z,y,v)* quotient(x,z,x1)* -> less_equal(w,divide(x1,y))*. % 14.12/14.35 122[0:Res:17.0,51.0] || -> equal(divide(u,zero),u)**. % 14.12/14.35 153[0:Res:10.1,52.0] || less_equal(u,v) -> equal(divide(u,v),zero)**. % 14.12/14.35 880[0:Res:17.0,107.0] || quotient(u,v,w)*+ quotient(x,v,y)* quotient(u,x,z)* -> less_equal(divide(w,y),divide(z,v))*. % 14.12/14.35 3105[0:Res:7.0,880.0] || quotient(u,y__dfg,v)*+ quotient(z__dfg,u,w)* -> less_equal(divide(zQy,v),divide(w,y__dfg))*. % 14.12/14.35 9287[0:Res:17.0,3105.0] || quotient(z__dfg,u,v)*+ -> less_equal(divide(zQy,divide(u,y__dfg)),divide(v,y__dfg))*. % 14.12/14.35 33972[0:Res:8.0,9287.0] || -> less_equal(divide(zQy,divide(x__dfg,y__dfg)),divide(zQx,y__dfg))*l. % 14.12/14.35 35384[0:SpR:153.1,33972.0] || less_equal(x__dfg,y__dfg) -> less_equal(divide(zQy,zero),divide(zQx,y__dfg))*r. % 14.12/14.35 35551[0:Rew:122.0,35384.1] || less_equal(x__dfg,y__dfg) -> less_equal(zQy,divide(zQx,y__dfg))*r. % 14.12/14.35 35552[0:MRR:35551.0,6.0] || -> less_equal(zQy,divide(zQx,y__dfg))*r. % 14.12/14.35 35720[0:OCh:5.1,5.0,35552.0,40.0] || -> less_equal(zQy,zQx)*r. % 14.12/14.35 35835[0:MRR:35720.0,9.0] || -> . % 14.12/14.35 % SZS output end Refutation % 14.12/14.35 Formulae used in the proof : x_divde_zero_is_x transitivity_of_less_equal xLEy zQy zQx prove_zQyLEzQx quotient_less_equal divisor_existence quotient_property closure well_defined % 14.12/14.35 %------------------------------------------------------------------------------