%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HEN006-2 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:04 EDT 2022 % Result : Unsatisfiable 40.03s 40.21s % Output : Refutation 40.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : HEN006-2 : TPTP v8.1.0. Released v1.0.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.33 % Computer : n027.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Fri Jul 1 13:11:37 EDT 2022 % 0.12/0.34 % CPUTime : % 40.03/40.21 % 40.03/40.21 SPASS V 3.9 % 40.03/40.21 SPASS beiseite: Proof found. % 40.03/40.21 % SZS status Theorem % 40.03/40.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 40.03/40.21 SPASS derived 63763 clauses, backtracked 0 clauses, performed 0 splits and kept 10284 clauses. % 40.03/40.21 SPASS allocated 113872 KBytes. % 40.03/40.21 SPASS spent 0:0:36.84 on the problem. % 40.03/40.21 0:00:00.04 for the input. % 40.03/40.21 0:00:00.00 for the FLOTTER CNF translation. % 40.03/40.21 0:00:00.75 for inferences. % 40.03/40.21 0:00:00.00 for the backtracking. % 40.03/40.21 0:0:35.91 for the reduction. % 40.03/40.21 % 40.03/40.21 % 40.03/40.21 Here is a proof with depth 11, length 69 : % 40.03/40.21 % SZS output start Refutation % 40.03/40.21 2[0:Inp] || -> quotient(zero,u,zero)*. % 40.03/40.21 4[0:Inp] || -> quotient(u,zero,u)*. % 40.03/40.21 5[0:Inp] || less_equal(u,v)* less_equal(v,w)* -> less_equal(u,w)*. % 40.03/40.21 6[0:Inp] || -> quotient(x__dfg,y__dfg,xQy)*. % 40.03/40.21 7[0:Inp] || -> less_equal(xQy,z__dfg)*r. % 40.03/40.21 8[0:Inp] || -> quotient(x__dfg,z__dfg,xQz)*. % 40.03/40.21 9[0:Inp] || less_equal(xQz,y__dfg)*l -> . % 40.03/40.21 10[0:Inp] || less_equal(u,v) -> quotient(u,v,zero)*. % 40.03/40.21 11[0:Inp] || quotient(u,v,zero)* -> less_equal(u,v). % 40.03/40.21 12[0:Inp] || quotient(u,v,w)* -> less_equal(w,u). % 40.03/40.21 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)*. % 40.03/40.22 14[0:Inp] || -> less_equal(zero,u)*. % 40.03/40.22 15[0:Inp] || less_equal(u,v)*+ less_equal(v,u)* -> equal(v,u). % 40.03/40.22 17[0:Inp] || -> quotient(u,v,divide(u,v))*. % 40.03/40.22 18[0:Inp] || quotient(u,v,w)*+ quotient(u,v,x)* -> equal(x,w)*. % 40.03/40.22 19[0:Res:11.1,9.0] || quotient(xQz,y__dfg,zero)* -> . % 40.03/40.22 40[0:Res:17.0,12.0] || -> less_equal(divide(u,v),u)*l. % 40.03/40.22 51[0:Res:4.0,18.0] || quotient(u,zero,v)* -> equal(v,u). % 40.03/40.22 52[0:Res:17.0,18.0] || quotient(u,v,w)* -> equal(w,divide(u,v)). % 40.03/40.22 65[0:Res:14.0,15.0] || less_equal(u,zero)* -> equal(u,zero). % 40.03/40.22 81[0:NCh:5.2,5.1,15.0,14.0] || equal(u,zero)* less_equal(v,u)*+ -> equal(v,u). % 40.03/40.22 102[0:Res:2.0,13.0] || quotient(u,v,w)*+ quotient(x,y,u)* quotient(z,y,v)* quotient(x,z,zero)* -> less_equal(w,zero). % 40.03/40.22 105[0:Res:4.0,13.0] || quotient(u,v,w)*+ quotient(x,zero,u)* quotient(y,zero,v)* quotient(x,y,z)* -> less_equal(w,z)*. % 40.03/40.22 106[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))*. % 40.03/40.22 107[0:Res:10.1,13.0] || less_equal(u,v)*+ quotient(w,x,y)* quotient(z,v,w)* quotient(x1,v,x)* quotient(z,x1,u)* -> less_equal(y,zero). % 40.03/40.22 121[0:Res:17.0,51.0] || -> equal(divide(u,zero),u)**. % 40.03/40.22 133[0:Res:40.0,15.0] || less_equal(u,divide(u,v))*r -> equal(divide(u,v),u). % 40.03/40.22 148[0:Res:10.1,52.0] || less_equal(u,v) -> equal(divide(u,v),zero)**. % 40.03/40.22 176[0:NCh:5.2,5.0,65.0,40.0] || equal(u,zero) -> equal(divide(u,v),zero)**. % 40.03/40.22 191[0:SpR:176.1,17.0] || equal(u,zero) -> quotient(u,v,zero)*. % 40.03/40.22 366[0:NCh:5.2,5.0,81.1,40.0] || equal(u,zero) equal(v,u) -> equal(divide(v,w),u)*. % 40.03/40.22 514[0:SpR:366.2,17.0] || equal(u,zero) equal(v,u) -> quotient(v,w,u)*. % 40.03/40.22 525[0:SpR:366.2,17.0] || equal(divide(u,v),zero) equal(w,divide(u,v)) -> quotient(u,v,divide(w,x))*. % 40.03/40.22 829[0:Res:4.0,105.0] || quotient(u,zero,v)*+ quotient(w,zero,zero)* quotient(u,w,x)* -> less_equal(v,x)*. % 40.03/40.22 886[0:Res:17.0,102.0] || quotient(u,v,w)*+ quotient(x,v,y)* quotient(u,x,zero)* -> less_equal(divide(w,y),zero)*l. % 40.03/40.22 974[0:Res:17.0,106.0] || quotient(u,v,w)*+ quotient(x,v,y)* quotient(u,x,z)* -> less_equal(divide(w,y),divide(z,v))*. % 40.03/40.22 999[0:Res:40.0,107.0] || quotient(u,v,w)* quotient(x,y,u)* quotient(z,y,v)* quotient(x,z,divide(y,x1))*+ -> less_equal(w,zero). % 40.03/40.22 1179[0:SpL:366.2,133.0] || equal(u,zero)* equal(v,u) less_equal(v,u)* -> equal(divide(v,w),v)**. % 40.03/40.22 2526[0:Res:4.0,829.0] || quotient(u,zero,zero)*+ quotient(v,u,w)* -> less_equal(v,w). % 40.03/40.22 3187[0:Res:17.0,886.0] || quotient(u,v,w)*+ quotient(x,u,zero)* -> less_equal(divide(divide(x,v),w),zero)*l. % 40.03/40.22 3319[0:Res:8.0,974.0] || quotient(u,z__dfg,v)*+ quotient(x__dfg,u,w)* -> less_equal(divide(xQz,v),divide(w,z__dfg))*. % 40.03/40.22 3580[0:Res:4.0,999.3] || quotient(u,v,w)* quotient(divide(x,y),x,u)*+ quotient(zero,x,v)* -> less_equal(w,zero). % 40.03/40.22 3714[0:Res:2.0,2526.0] || quotient(u,zero,v)* -> less_equal(u,v). % 40.03/40.22 3718[0:Res:191.1,2526.0] || equal(u,zero) quotient(v,u,w)* -> less_equal(v,w). % 40.03/40.22 3735[0:Res:514.2,3714.0] || equal(u,zero)*+ equal(v,u)* -> less_equal(v,u). % 40.03/40.22 3739[0:MRR:1179.2,3735.2] || equal(u,zero)*+ equal(v,u)* -> equal(divide(v,w),v)**. % 40.03/40.22 3766[0:Rew:3739.2,525.2] || equal(divide(u,v),zero) equal(w,divide(u,v)) -> quotient(u,v,w)*. % 40.03/40.22 3884[0:Res:3766.2,19.0] || equal(divide(xQz,y__dfg),zero)** equal(divide(xQz,y__dfg),zero)** -> . % 40.03/40.22 4027[0:Obv:3884.0] || equal(divide(xQz,y__dfg),zero)** -> . % 40.03/40.22 4671[0:Res:17.0,3718.1] || equal(u,zero) -> less_equal(v,divide(v,u))*r. % 40.03/40.22 4716[0:Res:4671.1,133.0] || equal(u,zero) -> equal(divide(v,u),v)**. % 40.03/40.22 4918[0:SpR:4716.1,148.1] || equal(u,zero)* less_equal(v,u)*+ -> equal(v,zero)*. % 40.03/40.22 7906[0:Res:17.0,3319.0] || quotient(x__dfg,u,v)*+ -> less_equal(divide(xQz,divide(u,z__dfg)),divide(v,z__dfg))*. % 40.03/40.22 7991[0:Res:17.0,3187.0] || quotient(u,v,zero) -> less_equal(divide(divide(u,w),divide(v,w)),zero)*l. % 40.03/40.22 11923[0:Res:17.0,3580.1] || quotient(divide(divide(u,v),u),w,x)* quotient(zero,u,w) -> less_equal(x,zero). % 40.03/40.22 31039[0:Res:6.0,7906.0] || -> less_equal(divide(xQz,divide(y__dfg,z__dfg)),divide(xQy,z__dfg))*l. % 40.03/40.22 32142[0:Res:31039.0,4918.1] || equal(divide(xQy,z__dfg),zero) -> equal(divide(xQz,divide(y__dfg,z__dfg)),zero)**. % 40.03/40.22 32384[0:SpR:32142.1,17.0] || equal(divide(xQy,z__dfg),zero) -> quotient(xQz,divide(y__dfg,z__dfg),zero)*. % 40.03/40.22 39669[0:Res:7991.1,65.0] || quotient(u,v,zero) -> equal(divide(divide(u,w),divide(v,w)),zero)**. % 40.03/40.22 52299[0:Res:4.0,11923.0] || quotient(zero,u,zero) -> less_equal(divide(divide(u,v),u),zero)*l. % 40.03/40.22 52320[0:MRR:52299.0,2.0] || -> less_equal(divide(divide(u,v),u),zero)*l. % 40.03/40.22 52940[0:Res:52320.0,65.0] || -> equal(divide(divide(u,v),u),zero)**. % 40.03/40.22 53317[0:SpR:52940.0,39669.1] || quotient(u,divide(v,w),zero)* -> equal(divide(divide(u,v),zero),zero). % 40.03/40.22 53692[0:Rew:121.0,53317.1] || quotient(u,divide(v,w),zero)* -> equal(divide(u,v),zero). % 40.03/40.22 82925[0:Res:32384.1,53692.0] || equal(divide(xQy,z__dfg),zero) -> equal(divide(xQz,y__dfg),zero)**. % 40.03/40.22 82952[0:MRR:82925.1,4027.0] || equal(divide(xQy,z__dfg),zero)** -> . % 40.03/40.22 82962[0:SpL:148.1,82952.0] || less_equal(xQy,z__dfg)*r equal(zero,zero) -> . % 40.03/40.22 82975[0:Obv:82962.1] || less_equal(xQy,z__dfg)*r -> . % 40.03/40.22 82976[0:MRR:82975.0,7.0] || -> . % 40.03/40.22 % SZS output end Refutation % 40.03/40.22 Formulae used in the proof : zero_divide_anything_is_zero x_divde_zero_is_x transitivity_of_less_equal xQy xQyLEz xQz prove_xQzLEy quotient_less_equal less_equal_quotient divisor_existence quotient_property zero_is_smallest less_equal_and_equal closure well_defined % 40.03/40.22 %------------------------------------------------------------------------------