%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HEN011-4 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:15 EDT 2022 % Result : Unsatisfiable 2.56s 2.76s % Output : Refutation 2.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : HEN011-4 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n018.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.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 14:15:02 EDT 2022 % 0.12/0.33 % CPUTime : % 2.56/2.76 % 2.56/2.76 SPASS V 3.9 % 2.56/2.76 SPASS beiseite: Proof found. % 2.56/2.76 % SZS status Theorem % 2.56/2.76 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.56/2.76 SPASS derived 8525 clauses, backtracked 0 clauses, performed 0 splits and kept 1831 clauses. % 2.56/2.76 SPASS allocated 70602 KBytes. % 2.56/2.76 SPASS spent 0:00:02.36 on the problem. % 2.56/2.76 0:00:00.04 for the input. % 2.56/2.76 0:00:00.00 for the FLOTTER CNF translation. % 2.56/2.76 0:00:00.08 for inferences. % 2.56/2.76 0:00:00.00 for the backtracking. % 2.56/2.76 0:00:02.21 for the reduction. % 2.56/2.76 % 2.56/2.76 % 2.56/2.76 Here is a proof with depth 3, length 25 : % 2.56/2.76 % SZS output start Refutation % 2.56/2.76 5[0:Inp] || less_equal(u,v)* less_equal(v,w)* -> less_equal(u,w)*. % 2.56/2.76 6[0:Inp] || less_equal(divide(u,v),w)*+ -> less_equal(divide(u,w),v)*. % 2.56/2.76 7[0:Inp] || less_equal(u,v) -> less_equal(divide(w,v),divide(w,u))*. % 2.56/2.76 9[0:Inp] || -> equal(divide(identity,divide(identity,divide(identity,u))),divide(identity,u))**. % 2.56/2.76 10[0:Inp] || -> equal(divide(divide(identity,u),divide(identity,divide(identity,u))),divide(identity,u))**. % 2.56/2.76 11[0:Inp] || equal(divide(divide(identity,b),divide(identity,divide(identity,a))),divide(divide(identity,a),divide(identity,divide(identity,b))))** -> . % 2.56/2.76 14[0:Inp] || -> less_equal(divide(u,v),u)*l. % 2.56/2.76 15[0:Inp] || -> less_equal(divide(divide(u,v),divide(w,v)),divide(divide(u,w),v))*l. % 2.56/2.76 17[0:Inp] || less_equal(u,v)*+ less_equal(v,u)* -> equal(v,u). % 2.56/2.76 20[0:Res:17.2,11.0] || less_equal(divide(divide(identity,b),divide(identity,divide(identity,a))),divide(divide(identity,a),divide(identity,divide(identity,b))))*l less_equal(divide(divide(identity,a),divide(identity,divide(identity,b))),divide(divide(identity,b),divide(identity,divide(identity,a)))) -> . % 2.56/2.76 120[0:SpR:10.0,15.0] || -> less_equal(divide(divide(identity,u),divide(v,divide(identity,divide(identity,u)))),divide(divide(divide(identity,u),v),divide(identity,divide(identity,u))))*r. % 2.56/2.76 210[0:Res:14.0,17.0] || less_equal(u,divide(u,v))*r -> equal(divide(u,v),u). % 2.56/2.76 218[0:NCh:5.2,5.0,17.0,14.0] || less_equal(u,v) less_equal(v,divide(u,w))* -> equal(v,divide(u,w)). % 2.56/2.76 510[0:Res:15.0,6.0] || -> less_equal(divide(divide(u,v),divide(divide(u,w),v)),divide(w,v))*l. % 2.56/2.76 512[0:Res:7.1,6.0] || less_equal(u,v)*+ -> less_equal(divide(w,divide(w,u)),v)*. % 2.56/2.76 2658[0:SpR:9.0,510.0] || -> less_equal(divide(divide(identity,u),divide(divide(identity,v),divide(identity,divide(identity,u)))),divide(v,divide(identity,divide(identity,u))))*l. % 2.56/2.76 4996[0:Res:14.0,512.0] || -> less_equal(divide(u,divide(u,divide(v,w))),v)*l. % 2.56/2.76 5822[0:Res:4996.0,6.0] || -> less_equal(divide(u,v),divide(u,divide(v,w)))*r. % 2.56/2.76 12555[0:Res:120.0,218.1] || less_equal(divide(divide(identity,u),v),divide(divide(identity,u),divide(v,divide(identity,divide(identity,u))))) -> equal(divide(divide(divide(identity,u),v),divide(identity,divide(identity,u))),divide(divide(identity,u),divide(v,divide(identity,divide(identity,u)))))**. % 2.56/2.76 12588[0:NCh:5.2,5.1,120.0,210.0] || less_equal(divide(divide(identity,u),v),divide(divide(identity,u),divide(v,divide(identity,divide(identity,u))))) -> equal(divide(divide(divide(identity,u),v),divide(identity,divide(identity,u))),divide(divide(identity,u),v))**. % 2.56/2.76 12692[0:MRR:12588.0,5822.0] || -> equal(divide(divide(divide(identity,u),v),divide(identity,divide(identity,u))),divide(divide(identity,u),v))**. % 2.56/2.76 12728[0:Rew:12692.0,12555.1] || less_equal(divide(divide(identity,u),v),divide(divide(identity,u),divide(v,divide(identity,divide(identity,u)))))*r -> equal(divide(divide(identity,u),divide(v,divide(identity,divide(identity,u)))),divide(divide(identity,u),v)). % 2.56/2.76 12729[0:MRR:12728.0,5822.0] || -> equal(divide(divide(identity,u),divide(v,divide(identity,divide(identity,u)))),divide(divide(identity,u),v))**. % 2.56/2.76 12771[0:Rew:12729.0,2658.0] || -> less_equal(divide(divide(identity,u),divide(identity,v)),divide(v,divide(identity,divide(identity,u))))*. % 2.56/2.76 12792[0:MRR:20.1,20.0,12771.0] || -> . % 2.56/2.76 % SZS output end Refutation % 2.56/2.76 Formulae used in the proof : transitivity_of_less_equal property_of_divide1 property_of_divide2 one_inversion_equals_three property_of_inversion prove_this quotient_smaller_than_numerator quotient_property less_equal_and_equal % 2.56/2.76 %------------------------------------------------------------------------------