%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HEN010-5 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:45:30 PM UTC 2026
% Result : Unsatisfiable 2.98s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN010-5 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 20:49:20 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 2.98/0.81 % Refutation found
% 2.98/0.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.98/0.81 % SZS output start CNFRefutation for theBenchmark
% 2.98/0.81 fof(f1,axiom,(
% 2.98/0.81 (![X,Y]: (divide(divide(X,Y),X) = zero ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f2,axiom,(
% 2.98/0.81 (![X,Z,Y]: (divide(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)) = zero ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f3,axiom,(
% 2.98/0.81 (![X]: (divide(zero,X) = zero ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f4,axiom,(
% 2.98/0.81 (![X,Y]: (( divide(X,Y) != zero| divide(Y,X) != zero| X = Y ) ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f7,axiom,(
% 2.98/0.81 (![X,Y,Z]: (( divide(divide(X,Y),Z) != zero| divide(divide(X,Z),Y) = zero ) ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f8,axiom,(
% 2.98/0.81 (![X,Y,Z]: (( divide(X,Y) != zero| divide(divide(X,Z),divide(Y,Z)) = zero ) ))),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f9,negated_conjecture,(
% 2.98/0.81 divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))) ),
% 2.98/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.98/0.81 fof(f10,plain,(
% 2.98/0.81 ![X0,X1]: (divide(divide(X0,X1),X0)=zero)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f1])).
% 2.98/0.81 fof(f11,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1))=zero)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f2])).
% 2.98/0.81 fof(f12,plain,(
% 2.98/0.81 ![X0]: (divide(zero,X0)=zero)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f3])).
% 2.98/0.81 fof(f13,plain,(
% 2.98/0.81 ![X0,X1]: (~divide(X0,X1)=zero|~divide(X1,X0)=zero|X0=X1)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f4])).
% 2.98/0.81 fof(f17,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(X0,X1),X2)=zero|divide(divide(X0,X2),X1)=zero)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f7])).
% 2.98/0.81 fof(f18,plain,(
% 2.98/0.81 ![X,Y]: (~divide(X,Y)=zero|(![Z]: divide(divide(X,Z),divide(Y,Z))=zero))),
% 2.98/0.81 inference(miniscoping,[status(thm)],[f8])).
% 2.98/0.81 fof(f19,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(X0,X1)=zero|divide(divide(X0,X2),divide(X1,X2))=zero)),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f18])).
% 2.98/0.81 fof(f20,plain,(
% 2.98/0.81 ~divide(identity,a)=divide(divide(identity,a),divide(identity,divide(identity,a)))),
% 2.98/0.81 inference(cnf_transformation,[status(thm)],[f9])).
% 2.98/0.81 fof(f34,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),zero),divide(divide(X0,divide(X1,X2)),X1))=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f10,f11])).
% 2.98/0.81 fof(f55,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2)))=zero|divide(divide(X0,X2),divide(X1,X2))=divide(divide(X0,X1),X2))),
% 2.98/0.81 inference(resolution,[status(thm)],[f13,f11])).
% 2.98/0.81 fof(f56,plain,(
% 2.98/0.81 ![X0,X1]: (~divide(X0,divide(X0,X1))=zero|divide(X0,X1)=X0)),
% 2.98/0.81 inference(resolution,[status(thm)],[f13,f10])).
% 2.98/0.81 fof(f58,plain,(
% 2.98/0.81 ![X0]: (~divide(X0,zero)=zero|zero=X0)),
% 2.98/0.81 inference(resolution,[status(thm)],[f13,f12])).
% 2.98/0.81 fof(f69,definition,(
% 2.98/0.81 sQ0_spl <=> (zero=zero)),
% 2.98/0.81 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.98/0.81 fof(f71,plain,(
% 2.98/0.81 ~zero=zero|sQ0_spl),
% 2.98/0.81 inference(component_clause,[status(thm)],[f69])).
% 2.98/0.81 fof(f88,plain,(
% 2.98/0.81 $false|sQ0_spl),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f71])).
% 2.98/0.81 fof(f89,plain,(
% 2.98/0.81 sQ0_spl),
% 2.98/0.81 inference(contradiction_clause,[status(thm)],[f88])).
% 2.98/0.81 fof(f130,plain,(
% 2.98/0.81 ![X0,X1]: (divide(divide(X0,X0),X1)=zero)),
% 2.98/0.81 inference(resolution,[status(thm)],[f17,f10])).
% 2.98/0.81 fof(f135,plain,(
% 2.98/0.81 ![X0,X1,X2,X3]: (~divide(zero,X0)=zero|divide(divide(divide(divide(X1,X2),divide(X3,X2)),X0),divide(divide(X1,X3),X2))=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f11,f17])).
% 2.98/0.81 fof(f136,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(zero,X0)=zero|divide(divide(divide(X1,X2),X0),X1)=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f10,f17])).
% 2.98/0.81 fof(f153,plain,(
% 2.98/0.81 ![X0,X1,X2,X3]: (~zero=zero|divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(X0,X2),X1))=zero)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f12,f135])).
% 2.98/0.81 fof(f154,plain,(
% 2.98/0.81 ![X0,X1,X2,X3]: (divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(X0,X2),X1))=zero)),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f153])).
% 2.98/0.81 fof(f155,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(divide(X0,X1),X2),X0)=zero)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f12,f136])).
% 2.98/0.81 fof(f156,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),X0)=zero)),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f155])).
% 2.98/0.81 fof(f162,plain,(
% 2.98/0.81 ![X0]: (zero=divide(X0,X0))),
% 2.98/0.81 inference(resolution,[status(thm)],[f130,f58])).
% 2.98/0.81 fof(f222,plain,(
% 2.98/0.81 ![X0,X1,X2,X3]: (divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))=zero)),
% 2.98/0.81 inference(resolution,[status(thm)],[f19,f11])).
% 2.98/0.81 fof(f223,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),divide(X0,X2))=zero)),
% 2.98/0.81 inference(resolution,[status(thm)],[f19,f10])).
% 2.98/0.81 fof(f251,plain,(
% 2.98/0.81 ![X0,X1]: (divide(divide(X0,divide(X0,X1)),X1)=zero)),
% 2.98/0.81 inference(resolution,[status(thm)],[f162,f17])).
% 2.98/0.81 fof(f592,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero))=zero|divide(divide(X0,divide(X1,X2)),X1)=divide(divide(X0,X1),zero))),
% 2.98/0.81 inference(resolution,[status(thm)],[f34,f13])).
% 2.98/0.81 fof(f703,plain,(
% 2.98/0.81 ![X0]: (zero=divide(X0,divide(X0,zero)))),
% 2.98/0.81 inference(resolution,[status(thm)],[f251,f58])).
% 2.98/0.81 fof(f923,plain,(
% 2.98/0.81 ![X0]: (~divide(divide(X0,zero),X0)=zero|divide(X0,zero)=X0)),
% 2.98/0.81 inference(resolution,[status(thm)],[f703,f13])).
% 2.98/0.81 fof(f962,plain,(
% 2.98/0.81 ![X0]: (~zero=zero|divide(X0,zero)=X0)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f10,f923])).
% 2.98/0.81 fof(f1007,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero))=zero|divide(divide(X0,divide(X1,X2)),X1)=divide(X0,X1))),
% 2.98/0.81 inference(backward_demodulation,[status(thm)],[f1017,f592])).
% 2.98/0.81 fof(f1017,plain,(
% 2.98/0.81 ![X0]: (divide(X0,zero)=X0)),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f962])).
% 2.98/0.81 fof(f1157,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,divide(X1,X2)),X1),divide(X0,X1))=zero|divide(divide(X0,divide(X1,X2)),X1)=divide(X0,X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1017,f1007])).
% 2.98/0.81 fof(f1158,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,divide(X1,X2)),X1)=divide(X0,X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f223,f1157])).
% 2.98/0.81 fof(f1163,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(X0,divide(X1,X2)),X1)=divide(X0,X1))),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f1158])).
% 2.98/0.81 fof(f1200,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,divide(X1,divide(X1,X2))),X2),divide(divide(X0,X2),zero))=zero|divide(divide(X0,X2),divide(divide(X1,divide(X1,X2)),X2))=divide(divide(X0,divide(X1,divide(X1,X2))),X2))),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f251,f55])).
% 2.98/0.81 fof(f1204,plain,(
% 2.98/0.81 ![X0,X1]: (~divide(divide(divide(X0,X1),X1),divide(divide(X0,X1),zero))=zero|divide(divide(X0,X1),divide(X1,X1))=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f162,f55])).
% 2.98/0.81 fof(f1306,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,divide(X1,divide(X1,X2))),X2),divide(X0,X2))=zero|divide(divide(X0,X2),divide(divide(X1,divide(X1,X2)),X2))=divide(divide(X0,divide(X1,divide(X1,X2))),X2))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1017,f1200])).
% 2.98/0.81 fof(f1307,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,X1),divide(divide(X2,divide(X2,X1)),X1))=divide(divide(X0,divide(X2,divide(X2,X1))),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f223,f1306])).
% 2.98/0.81 fof(f1308,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,X1),zero)=divide(divide(X0,divide(X2,divide(X2,X1))),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f251,f1307])).
% 2.98/0.81 fof(f1309,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(X0,X1)=divide(divide(X0,divide(X2,divide(X2,X1))),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1017,f1308])).
% 2.98/0.81 fof(f1312,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,divide(X2,divide(X2,X1))),X1))),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f1309])).
% 2.98/0.81 fof(f1327,plain,(
% 2.98/0.81 ![X0,X1]: (~divide(divide(divide(X0,X1),X1),divide(X0,X1))=zero|divide(divide(X0,X1),divide(X1,X1))=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1017,f1204])).
% 2.98/0.81 fof(f1328,plain,(
% 2.98/0.81 ![X0,X1]: (~zero=zero|divide(divide(X0,X1),divide(X1,X1))=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f10,f1327])).
% 2.98/0.81 fof(f1329,plain,(
% 2.98/0.81 ![X0,X1]: (~zero=zero|divide(divide(X0,X1),zero)=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f162,f1328])).
% 2.98/0.81 fof(f1330,plain,(
% 2.98/0.81 ![X0,X1]: (~zero=zero|divide(X0,X1)=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1017,f1329])).
% 2.98/0.81 fof(f1333,plain,(
% 2.98/0.81 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1))),
% 2.98/0.81 inference(trivial_equality_resolution,[status(thm)],[f1330])).
% 2.98/0.81 fof(f1569,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1)))=zero|divide(divide(divide(X0,X1),X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1))),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f1333,f55])).
% 2.98/0.81 fof(f1595,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1)))=zero|divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1))),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f1333,f1569])).
% 2.98/0.81 fof(f2618,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1))=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f1163,f154])).
% 2.98/0.81 fof(f2654,plain,(
% 2.98/0.81 ![X0,X1,X2,X3]: (divide(divide(divide(X0,X1),X2),divide(X0,divide(X1,X3)))=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f1163,f156])).
% 2.98/0.81 fof(f2691,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1))),
% 2.98/0.81 inference(backward_demodulation,[status(thm)],[f2654,f1595])).
% 2.98/0.81 fof(f2696,definition,(
% 2.98/0.81 ![X0,X1,X2]: (sQ99_spl <=> (divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1)))),
% 2.98/0.81 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 2.98/0.81 fof(f2697,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1)|~sQ99_spl)),
% 2.98/0.81 inference(component_clause,[status(thm)],[f2696])).
% 2.98/0.81 fof(f2699,plain,(
% 2.98/0.81 ~sQ0_spl|sQ99_spl),
% 2.98/0.81 inference(split_clause,[status(thm)],[f2691,f69,f2696])).
% 2.98/0.81 fof(f2727,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),divide(divide(divide(X0,X2),X1),X2))=zero)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f1163,f222])).
% 2.98/0.81 fof(f2848,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1)|~sQ99_spl)),
% 2.98/0.81 inference(backward_demodulation,[status(thm)],[f2849,f55])).
% 2.98/0.81 fof(f2849,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2)))=zero|~sQ99_spl)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f2697,f2727])).
% 2.98/0.81 fof(f3028,definition,(
% 2.98/0.81 ![X0,X1,X2]: (sQ107_spl <=> (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1)))),
% 2.98/0.81 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 2.98/0.81 fof(f3029,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1)|~sQ107_spl)),
% 2.98/0.81 inference(component_clause,[status(thm)],[f3028])).
% 2.98/0.81 fof(f3031,plain,(
% 2.98/0.81 ~sQ0_spl|sQ107_spl|~sQ99_spl),
% 2.98/0.81 inference(split_clause,[status(thm)],[f2848,f69,f3028,f2696])).
% 2.98/0.81 fof(f3088,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(divide(divide(X0,X2),X1),X2)|~sQ107_spl|~sQ99_spl)),
% 2.98/0.81 inference(backward_demodulation,[status(thm)],[f3029,f2697])).
% 2.98/0.81 fof(f5051,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1))=zero|divide(divide(divide(X0,X1),X2),X1)=divide(divide(X0,X1),X2)|~sQ107_spl|~sQ99_spl)),
% 2.98/0.81 inference(paramodulation,[status(thm)],[f3088,f56])).
% 2.98/0.81 fof(f5128,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(divide(X0,X1),X2),X1)=divide(divide(X0,X1),X2)|~sQ107_spl|~sQ99_spl)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f2618,f5051])).
% 2.98/0.81 fof(f5129,plain,(
% 2.98/0.81 ![X0,X1,X2]: (~zero=zero|divide(divide(X0,X1),X2)=divide(divide(X0,X2),X1)|~sQ107_spl|~sQ99_spl)),
% 2.98/0.81 inference(forward_demodulation,[status(thm)],[f3088,f5128])).
% 2.98/0.81 fof(f5131,plain,(
% 2.98/0.81 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,X1),divide(X2,divide(X2,X1)))|~sQ107_spl|~sQ99_spl)),
% 2.98/0.82 inference(backward_demodulation,[status(thm)],[f5162,f1312])).
% 2.98/0.82 fof(f5162,plain,(
% 2.98/0.82 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(divide(X0,X2),X1)|~sQ107_spl|~sQ99_spl)),
% 2.98/0.82 inference(trivial_equality_resolution,[status(thm)],[f5129])).
% 2.98/0.82 fof(f5164,plain,(
% 2.98/0.82 ~divide(identity,a)=divide(identity,a)|~sQ107_spl|~sQ99_spl),
% 2.98/0.82 inference(backward_demodulation,[status(thm)],[f5131,f20])).
% 2.98/0.82 fof(f5183,plain,(
% 2.98/0.82 $false|~sQ107_spl|~sQ99_spl),
% 2.98/0.82 inference(trivial_equality_resolution,[status(thm)],[f5164])).
% 2.98/0.82 fof(f5184,plain,(
% 2.98/0.82 ~sQ107_spl|~sQ99_spl),
% 2.98/0.82 inference(contradiction_clause,[status(thm)],[f5183])).
% 2.98/0.82 fof(f5185,plain,(
% 2.98/0.82 $false),
% 2.98/0.82 inference(sat_refutation,[status(thm)],[f89,f2699,f3031,f5184])).
% 2.98/0.82 % SZS output end CNFRefutation for theBenchmark.p
% 2.98/0.83 % Elapsed time: 0.448891 seconds
% 2.98/0.83 % CPU time: 3.335233 seconds
% 2.98/0.83 % Total memory used: 119.350 MB
% 2.98/0.83 % Net memory used: 115.318 MB
%------------------------------------------------------------------------------