%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 11.14s 1.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:46:07 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 11.14/1.88 % Refutation found
% 11.14/1.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.14/1.88 % SZS output start CNFRefutation for theBenchmark
% 11.14/1.88 fof(f1,axiom,(
% 11.14/1.88 (![X,Y]: (( ~ less_equal(X,Y)| divide(X,Y) = zero ) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f2,axiom,(
% 11.14/1.88 (![X,Y]: (( divide(X,Y) != zero| less_equal(X,Y) ) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f3,axiom,(
% 11.14/1.88 (![X,Y]: (less_equal(divide(X,Y),X) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f4,axiom,(
% 11.14/1.88 (![X,Z,Y]: (less_equal(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f5,axiom,(
% 11.14/1.88 (![X]: (less_equal(zero,X) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f6,axiom,(
% 11.14/1.88 (![X,Y]: (( ~ less_equal(X,Y)| ~ less_equal(Y,X)| X = Y ) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f7,axiom,(
% 11.14/1.88 (![X]: (less_equal(X,identity) ))),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f9,hypothesis,(
% 11.14/1.88 divide(identity,a) = c ),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f10,hypothesis,(
% 11.14/1.88 divide(identity,b) = d ),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f11,hypothesis,(
% 11.14/1.88 divide(identity,c) = e ),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f12,hypothesis,(
% 11.14/1.88 divide(identity,d) = g ),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f13,negated_conjecture,(
% 11.14/1.88 divide(c,g) != divide(d,e) ),
% 11.14/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.14/1.88 fof(f14,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(X0,X1)|divide(X0,X1)=zero)),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f1])).
% 11.14/1.88 fof(f15,plain,(
% 11.14/1.88 ![X0,X1]: (~divide(X0,X1)=zero|less_equal(X0,X1))),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f2])).
% 11.14/1.88 fof(f16,plain,(
% 11.14/1.88 ![X0,X1]: (less_equal(divide(X0,X1),X0))),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f3])).
% 11.14/1.88 fof(f17,plain,(
% 11.14/1.88 ![X0,X1,X2]: (less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)))),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f4])).
% 11.14/1.88 fof(f18,plain,(
% 11.14/1.88 ![X0]: (less_equal(zero,X0))),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f5])).
% 11.14/1.88 fof(f19,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(X0,X1)|~less_equal(X1,X0)|X0=X1)),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f6])).
% 11.14/1.88 fof(f20,plain,(
% 11.14/1.88 ![X0]: (less_equal(X0,identity))),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f7])).
% 11.14/1.88 fof(f22,plain,(
% 11.14/1.88 divide(identity,a)=c),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f9])).
% 11.14/1.88 fof(f23,plain,(
% 11.14/1.88 divide(identity,b)=d),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f10])).
% 11.14/1.88 fof(f24,plain,(
% 11.14/1.88 divide(identity,c)=e),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f11])).
% 11.14/1.88 fof(f25,plain,(
% 11.14/1.88 divide(identity,d)=g),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f12])).
% 11.14/1.88 fof(f26,plain,(
% 11.14/1.88 ~divide(c,g)=divide(d,e)),
% 11.14/1.88 inference(cnf_transformation,[status(thm)],[f13])).
% 11.14/1.88 fof(f34,plain,(
% 11.14/1.88 ![X0,X1]: (divide(divide(X0,X1),X0)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f14,f16])).
% 11.14/1.88 fof(f35,plain,(
% 11.14/1.88 ![X0]: (divide(zero,X0)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f14,f18])).
% 11.14/1.88 fof(f36,plain,(
% 11.14/1.88 ![X0]: (divide(X0,identity)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f14,f20])).
% 11.14/1.88 fof(f55,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(X0,divide(X0,X1))|X0=divide(X0,X1))),
% 11.14/1.88 inference(resolution,[status(thm)],[f19,f16])).
% 11.14/1.88 fof(f56,plain,(
% 11.14/1.88 ![X0]: (~less_equal(X0,zero)|X0=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f19,f18])).
% 11.14/1.88 fof(f58,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(X0,X1)|X0=X1|~divide(X1,X0)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f19,f15])).
% 11.14/1.88 fof(f61,plain,(
% 11.14/1.88 ![X0]: (X0=zero|~divide(X0,zero)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f56,f15])).
% 11.14/1.88 fof(f62,plain,(
% 11.14/1.88 ![X0,X1,X2]: (~less_equal(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2)))|divide(divide(X0,X1),X2)=divide(divide(X0,X2),divide(X1,X2)))),
% 11.14/1.88 inference(resolution,[status(thm)],[f17,f19])).
% 11.14/1.88 fof(f63,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f17,f14])).
% 11.14/1.88 fof(f67,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(g,divide(X0,d)),divide(divide(identity,X0),d)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f25,f17])).
% 11.14/1.88 fof(f68,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(e,divide(X0,c)),divide(divide(identity,X0),c)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f24,f17])).
% 11.14/1.88 fof(f69,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(d,divide(X0,b)),divide(divide(identity,X0),b)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f23,f17])).
% 11.14/1.88 fof(f70,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(c,divide(X0,a)),divide(divide(identity,X0),a)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f17])).
% 11.14/1.88 fof(f72,plain,(
% 11.14/1.88 ![X0,X1,X2]: (less_equal(divide(divide(X0,X1),zero),divide(divide(X0,divide(X1,X2)),X1)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f17])).
% 11.14/1.88 fof(f73,plain,(
% 11.14/1.88 ![X0,X1]: (less_equal(divide(divide(X0,X1),zero),divide(divide(X0,zero),X1)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f35,f17])).
% 11.14/1.88 fof(f74,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,d),g),divide(divide(X0,identity),d)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f25,f17])).
% 11.14/1.88 fof(f75,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,c),e),divide(divide(X0,identity),c)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f24,f17])).
% 11.14/1.88 fof(f76,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,b),d),divide(divide(X0,identity),b)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f23,f17])).
% 11.14/1.88 fof(f77,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,a),c),divide(divide(X0,identity),a)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f17])).
% 11.14/1.88 fof(f86,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(identity,X0),divide(a,X0)),divide(c,X0)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f17])).
% 11.14/1.88 fof(f96,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,d),g),divide(zero,d)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f36,f74])).
% 11.14/1.88 fof(f97,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,d),g),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f96])).
% 11.14/1.88 fof(f98,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,c),e),divide(zero,c)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f36,f75])).
% 11.14/1.88 fof(f99,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,c),e),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f98])).
% 11.14/1.88 fof(f100,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,b),d),divide(zero,b)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f36,f76])).
% 11.14/1.88 fof(f101,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,b),d),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f100])).
% 11.14/1.88 fof(f102,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,a),c),divide(zero,a)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f36,f77])).
% 11.14/1.88 fof(f103,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,a),c),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f102])).
% 11.14/1.88 fof(f127,plain,(
% 11.14/1.88 ![X0,X1]: (X0=divide(X0,X1)|~divide(X0,divide(X0,X1))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f55,f15])).
% 11.14/1.88 fof(f141,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1)|~divide(divide(divide(X0,X2),X1),divide(divide(X0,X1),divide(X2,X1)))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f58,f17])).
% 11.14/1.88 fof(f145,plain,(
% 11.14/1.88 ![X0,X1]: (X0=X1|~divide(X1,X0)=zero|~divide(X0,X1)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f58,f15])).
% 11.14/1.88 fof(f146,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,d),g)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f97,f56])).
% 11.14/1.88 fof(f192,plain,(
% 11.14/1.88 ![X0]: (~less_equal(zero,divide(divide(X0,g),divide(d,g)))|divide(divide(X0,d),g)=divide(divide(X0,g),divide(d,g)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f146,f62])).
% 11.14/1.88 fof(f193,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(zero,divide(divide(X0,X0),divide(X1,X0)))|divide(divide(X0,X1),X0)=divide(divide(X0,X0),divide(X1,X0)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f62])).
% 11.14/1.88 fof(f197,plain,(
% 11.14/1.88 ![X0,X1,X2]: (~less_equal(divide(zero,X0),divide(divide(divide(X1,X2),X0),divide(X1,X0)))|divide(divide(divide(X1,X2),X1),X0)=divide(divide(divide(X1,X2),X0),divide(X1,X0)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f62])).
% 11.14/1.88 fof(f212,plain,(
% 11.14/1.88 ![X0]: (~less_equal(divide(divide(identity,X0),a),divide(c,divide(X0,a)))|divide(divide(identity,X0),a)=divide(divide(identity,a),divide(X0,a)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f62])).
% 11.14/1.88 fof(f223,plain,(
% 11.14/1.88 ![X0]: (~less_equal(zero,divide(divide(X0,g),divide(d,g)))|zero=divide(divide(X0,g),divide(d,g)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f146,f192])).
% 11.14/1.88 fof(f225,plain,(
% 11.14/1.88 ![X0]: (zero=divide(divide(X0,g),divide(d,g)))),
% 11.14/1.88 inference(forward_subsumption_resolution,[status(thm)],[f223,f18])).
% 11.14/1.88 fof(f226,plain,(
% 11.14/1.88 ![X0,X1]: (~less_equal(zero,divide(divide(X0,X0),divide(X1,X0)))|zero=divide(divide(X0,X0),divide(X1,X0)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f34,f193])).
% 11.14/1.88 fof(f228,plain,(
% 11.14/1.88 ![X0,X1]: (zero=divide(divide(X0,X0),divide(X1,X0)))),
% 11.14/1.88 inference(forward_subsumption_resolution,[status(thm)],[f226,f18])).
% 11.14/1.88 fof(f243,plain,(
% 11.14/1.88 ![X0,X1,X2]: (~less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2)))|divide(divide(divide(X0,X1),X0),X2)=divide(divide(divide(X0,X1),X2),divide(X0,X2)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f197])).
% 11.14/1.88 fof(f244,plain,(
% 11.14/1.88 ![X0,X1,X2]: (~less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2)))|divide(zero,X2)=divide(divide(divide(X0,X1),X2),divide(X0,X2)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f34,f243])).
% 11.14/1.88 fof(f245,plain,(
% 11.14/1.88 ![X0,X1,X2]: (~less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2)))|zero=divide(divide(divide(X0,X1),X2),divide(X0,X2)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f244])).
% 11.14/1.88 fof(f247,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),divide(X0,X2)))),
% 11.14/1.88 inference(forward_subsumption_resolution,[status(thm)],[f245,f18])).
% 11.14/1.88 fof(f285,plain,(
% 11.14/1.88 ![X0]: (~less_equal(divide(divide(identity,X0),a),divide(c,divide(X0,a)))|divide(divide(identity,X0),a)=divide(c,divide(X0,a)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f22,f212])).
% 11.14/1.88 fof(f323,plain,(
% 11.14/1.88 ![X0]: (zero=divide(divide(X0,X0),zero))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f228])).
% 11.14/1.88 fof(f364,plain,(
% 11.14/1.88 ![X0]: (divide(X0,X0)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f323,f61])).
% 11.14/1.88 fof(f469,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,c),e)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f99,f56])).
% 11.14/1.88 fof(f494,plain,(
% 11.14/1.88 ![X0]: (divide(divide(c,divide(X0,a)),divide(divide(identity,X0),a))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f63])).
% 11.14/1.88 fof(f518,plain,(
% 11.14/1.88 ![X0]: (divide(divide(divide(identity,X0),divide(b,X0)),divide(d,X0))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f23,f63])).
% 11.14/1.88 fof(f526,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (~less_equal(divide(zero,X0),divide(divide(divide(divide(X1,X2),divide(X3,X2)),X0),divide(divide(divide(X1,X3),X2),X0)))|divide(divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)),X0)=divide(divide(divide(divide(X1,X2),divide(X3,X2)),X0),divide(divide(divide(X1,X3),X2),X0)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f63,f62])).
% 11.14/1.88 fof(f564,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (~less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))|divide(divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),X3)=divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f526])).
% 11.14/1.88 fof(f565,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (~less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))|divide(zero,X3)=divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f63,f564])).
% 11.14/1.88 fof(f566,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (~less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))|zero=divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f565])).
% 11.14/1.88 fof(f568,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (zero=divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)))),
% 11.14/1.88 inference(forward_subsumption_resolution,[status(thm)],[f566,f18])).
% 11.14/1.88 fof(f579,plain,(
% 11.14/1.88 ![X0]: (~less_equal(zero,divide(divide(X0,e),divide(c,e)))|divide(divide(X0,c),e)=divide(divide(X0,e),divide(c,e)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f469,f62])).
% 11.14/1.88 fof(f594,plain,(
% 11.14/1.88 ![X0]: (~less_equal(zero,divide(divide(X0,e),divide(c,e)))|zero=divide(divide(X0,e),divide(c,e)))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f469,f579])).
% 11.14/1.88 fof(f596,plain,(
% 11.14/1.88 ![X0]: (zero=divide(divide(X0,e),divide(c,e)))),
% 11.14/1.88 inference(forward_subsumption_resolution,[status(thm)],[f594,f18])).
% 11.14/1.88 fof(f613,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,b),d)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f101,f56])).
% 11.14/1.88 fof(f671,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,a),c)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f103,f56])).
% 11.14/1.88 fof(f696,plain,(
% 11.14/1.88 less_equal(divide(g,divide(b,d)),zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f613,f67])).
% 11.14/1.88 fof(f909,plain,(
% 11.14/1.88 less_equal(divide(e,divide(a,c)),zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f671,f68])).
% 11.14/1.88 fof(f931,plain,(
% 11.14/1.88 divide(g,divide(b,d))=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f696,f56])).
% 11.14/1.88 fof(f938,plain,(
% 11.14/1.88 divide(b,d)=g|~divide(divide(b,d),g)=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f931,f145])).
% 11.14/1.88 fof(f955,plain,(
% 11.14/1.88 divide(b,d)=g|~zero=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f146,f938])).
% 11.14/1.88 fof(f958,plain,(
% 11.14/1.88 divide(b,d)=g),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f955])).
% 11.14/1.88 fof(f1007,plain,(
% 11.14/1.88 divide(g,b)=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f958,f34])).
% 11.14/1.88 fof(f1023,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,b))=divide(divide(identity,X0),b)|~divide(divide(divide(identity,X0),b),divide(d,divide(X0,b)))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f69,f58])).
% 11.14/1.88 fof(f1030,plain,(
% 11.14/1.88 less_equal(divide(d,divide(d,b)),divide(g,b))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f25,f69])).
% 11.14/1.88 fof(f1040,plain,(
% 11.14/1.88 less_equal(divide(d,divide(d,b)),zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1007,f1030])).
% 11.14/1.88 fof(f1095,plain,(
% 11.14/1.88 less_equal(divide(c,divide(c,a)),divide(e,a))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f24,f70])).
% 11.14/1.88 fof(f1114,plain,(
% 11.14/1.88 divide(e,divide(a,c))=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f909,f56])).
% 11.14/1.88 fof(f1121,plain,(
% 11.14/1.88 divide(a,c)=e|~divide(divide(a,c),e)=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f1114,f145])).
% 11.14/1.88 fof(f1138,plain,(
% 11.14/1.88 divide(a,c)=e|~zero=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f469,f1121])).
% 11.14/1.88 fof(f1141,plain,(
% 11.14/1.88 divide(a,c)=e),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f1138])).
% 11.14/1.88 fof(f1190,plain,(
% 11.14/1.88 divide(e,a)=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1141,f34])).
% 11.14/1.88 fof(f1206,plain,(
% 11.14/1.88 less_equal(divide(c,divide(c,a)),zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f1190,f1095])).
% 11.14/1.88 fof(f1305,plain,(
% 11.14/1.88 divide(d,divide(d,b))=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f1040,f56])).
% 11.14/1.88 fof(f1312,plain,(
% 11.14/1.88 d=divide(d,b)),
% 11.14/1.88 inference(resolution,[status(thm)],[f1305,f127])).
% 11.14/1.88 fof(f1543,plain,(
% 11.14/1.88 divide(c,divide(c,a))=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f1206,f56])).
% 11.14/1.88 fof(f1550,plain,(
% 11.14/1.88 c=divide(c,a)),
% 11.14/1.88 inference(resolution,[status(thm)],[f1543,f127])).
% 11.14/1.88 fof(f1659,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),zero)=divide(divide(X0,divide(X1,X2)),X1)|~divide(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f72,f58])).
% 11.14/1.88 fof(f1836,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(divide(X0,g),d),zero),divide(zero,d)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f225,f72])).
% 11.14/1.88 fof(f1863,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(divide(X0,g),d),zero),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f1836])).
% 11.14/1.88 fof(f1939,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(divide(X0,X1),X2),X0),zero))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f247])).
% 11.14/1.88 fof(f2059,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,divide(X0,zero)),zero),zero))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f364,f73])).
% 11.14/1.88 fof(f2114,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(divide(X0,e),c),zero),divide(zero,c)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f596,f72])).
% 11.14/1.88 fof(f2144,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(divide(X0,e),c),zero),zero))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f2114])).
% 11.14/1.88 fof(f2436,plain,(
% 11.14/1.88 ![X0]: (divide(divide(c,a),divide(X0,a))=divide(divide(c,X0),a)|~divide(divide(divide(c,X0),a),divide(c,divide(X0,a)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1550,f141])).
% 11.14/1.88 fof(f2437,plain,(
% 11.14/1.88 ![X0]: (divide(divide(d,b),divide(X0,b))=divide(divide(d,X0),b)|~divide(divide(divide(d,X0),b),divide(d,divide(X0,b)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1312,f141])).
% 11.14/1.88 fof(f2454,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X0),divide(X2,X0))=divide(divide(divide(X0,X1),X2),X0)|~divide(divide(divide(divide(X0,X1),X2),X0),divide(zero,divide(X2,X0)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f34,f141])).
% 11.14/1.88 fof(f2464,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,a),divide(e,a))=divide(divide(X0,e),a)|~divide(divide(divide(X0,e),a),divide(divide(X0,a),zero))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1190,f141])).
% 11.14/1.88 fof(f2466,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,b),divide(g,b))=divide(divide(X0,g),b)|~divide(divide(divide(X0,g),b),divide(divide(X0,b),zero))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1007,f141])).
% 11.14/1.88 fof(f2567,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,a))=divide(divide(c,X0),a)|~divide(divide(divide(c,X0),a),divide(c,divide(X0,a)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1550,f2436])).
% 11.14/1.88 fof(f2568,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,b))=divide(divide(d,X0),b)|~divide(divide(divide(d,X0),b),divide(d,divide(X0,b)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1312,f2437])).
% 11.14/1.88 fof(f2647,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(zero,divide(X0,X1))=divide(divide(divide(X1,X2),X0),X1)|~divide(divide(divide(divide(X1,X2),X0),X1),divide(zero,divide(X0,X1)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f34,f2454])).
% 11.14/1.88 fof(f2648,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),X0)|~divide(divide(divide(divide(X0,X1),X2),X0),divide(zero,divide(X2,X0)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f2647])).
% 11.14/1.88 fof(f2649,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),X0)|~divide(divide(divide(divide(X0,X1),X2),X0),zero)=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f35,f2648])).
% 11.14/1.88 fof(f2650,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),X0)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1939,f2649])).
% 11.14/1.88 fof(f2652,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),X0))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f2650])).
% 11.14/1.88 fof(f2670,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,a),zero)=divide(divide(X0,e),a)|~divide(divide(divide(X0,e),a),divide(divide(X0,a),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1190,f2464])).
% 11.14/1.88 fof(f2673,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,b),zero)=divide(divide(X0,g),b)|~divide(divide(divide(X0,g),b),divide(divide(X0,b),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f1007,f2466])).
% 11.14/1.88 fof(f3787,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,divide(X0,zero)),zero)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f2059,f56])).
% 11.14/1.88 fof(f3807,plain,(
% 11.14/1.88 ![X0]: (divide(X0,divide(X0,zero))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f3787,f61])).
% 11.14/1.88 fof(f3913,plain,(
% 11.14/1.88 ![X0]: (X0=divide(X0,zero))),
% 11.14/1.88 inference(resolution,[status(thm)],[f3807,f127])).
% 11.14/1.88 fof(f3971,plain,(
% 11.14/1.88 ![X0,X1]: (divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))=divide(divide(X0,X1),divide(X1,zero))|~divide(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f3807,f141])).
% 11.14/1.88 fof(f4048,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,e),c),zero))),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f3913,f2144])).
% 11.14/1.88 fof(f4049,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(divide(X0,g),d),zero))),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f3913,f1863])).
% 11.14/1.88 fof(f4056,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,a),zero)=divide(divide(X0,e),a)|~divide(divide(divide(X0,e),a),divide(X0,a))=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f3913,f2670])).
% 11.14/1.88 fof(f4067,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,b),zero)=divide(divide(X0,g),b)|~divide(divide(divide(X0,g),b),divide(X0,b))=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f3913,f2673])).
% 11.14/1.88 fof(f4137,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),zero)=divide(divide(X0,divide(X1,X2)),X1)|~divide(divide(divide(X0,divide(X1,X2)),X1),divide(X0,X1))=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f3913,f1659])).
% 11.14/1.88 fof(f4303,plain,(
% 11.14/1.88 ![X0,X1]: (divide(divide(X0,X1),divide(X1,divide(X1,zero)))=divide(divide(X0,X1),divide(X1,zero))|~divide(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f3971])).
% 11.14/1.88 fof(f4304,plain,(
% 11.14/1.88 ![X0,X1]: (divide(divide(X0,X1),zero)=divide(divide(X0,X1),divide(X1,zero))|~divide(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3807,f4303])).
% 11.14/1.88 fof(f4305,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),divide(X1,zero))|~divide(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4304])).
% 11.14/1.88 fof(f4306,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1)|~divide(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4305])).
% 11.14/1.88 fof(f4307,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1)|~divide(divide(divide(X0,X1),X1),divide(divide(X0,divide(X1,zero)),zero))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4306])).
% 11.14/1.88 fof(f4308,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1)|~divide(divide(divide(X0,X1),X1),divide(X0,divide(X1,zero)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4307])).
% 11.14/1.88 fof(f4309,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1)|~divide(divide(divide(X0,X1),X1),divide(X0,X1))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4308])).
% 11.14/1.88 fof(f4310,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f247,f4309])).
% 11.14/1.88 fof(f4311,plain,(
% 11.14/1.88 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),X1))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f4310])).
% 11.14/1.88 fof(f4457,plain,(
% 11.14/1.88 ![X0]: (divide(X0,a)=divide(divide(X0,e),a)|~divide(divide(divide(X0,e),a),divide(X0,a))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4056])).
% 11.14/1.88 fof(f4458,plain,(
% 11.14/1.88 ![X0]: (divide(X0,a)=divide(divide(X0,e),a)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f247,f4457])).
% 11.14/1.88 fof(f4459,plain,(
% 11.14/1.88 ![X0]: (divide(X0,a)=divide(divide(X0,e),a))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f4458])).
% 11.14/1.88 fof(f4475,plain,(
% 11.14/1.88 ![X0]: (divide(X0,b)=divide(divide(X0,g),b)|~divide(divide(divide(X0,g),b),divide(X0,b))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4067])).
% 11.14/1.88 fof(f4476,plain,(
% 11.14/1.88 ![X0]: (divide(X0,b)=divide(divide(X0,g),b)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f247,f4475])).
% 11.14/1.88 fof(f4477,plain,(
% 11.14/1.88 ![X0]: (divide(X0,b)=divide(divide(X0,g),b))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f4476])).
% 11.14/1.88 fof(f4602,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,divide(X1,X2)),X1)|~divide(divide(divide(X0,divide(X1,X2)),X1),divide(X0,X1))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f3913,f4137])).
% 11.14/1.88 fof(f4603,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,divide(X1,X2)),X1)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f247,f4602])).
% 11.14/1.88 fof(f4609,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,divide(X1,X2)),X1))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f4603])).
% 11.14/1.88 fof(f5232,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1)|~divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4311,f141])).
% 11.14/1.88 fof(f5302,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1)|~divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f4311,f5232])).
% 11.14/1.88 fof(f5307,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,e),c)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f4048,f56])).
% 11.14/1.88 fof(f5436,plain,(
% 11.14/1.88 ![X0]: (divide(divide(X0,g),d)=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f4049,f56])).
% 11.14/1.88 fof(f5855,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(X0,a),divide(X0,e)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4459,f16])).
% 11.14/1.88 fof(f6120,plain,(
% 11.14/1.88 less_equal(c,divide(c,e))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1550,f5855])).
% 11.14/1.88 fof(f6130,plain,(
% 11.14/1.88 less_equal(c,divide(identity,e))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f5855])).
% 11.14/1.88 fof(f6152,plain,(
% 11.14/1.88 c=divide(c,e)),
% 11.14/1.88 inference(resolution,[status(thm)],[f6120,f55])).
% 11.14/1.88 fof(f6180,plain,(
% 11.14/1.88 ![X0]: (divide(divide(c,e),divide(X0,e))=divide(divide(c,X0),e)|~divide(divide(divide(c,X0),e),divide(c,divide(X0,e)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6152,f141])).
% 11.14/1.88 fof(f6209,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,e))=divide(divide(c,X0),e)|~divide(divide(divide(c,X0),e),divide(c,divide(X0,e)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f6152,f6180])).
% 11.14/1.88 fof(f6221,plain,(
% 11.14/1.88 c=divide(identity,e)|~divide(divide(identity,e),c)=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f6130,f58])).
% 11.14/1.88 fof(f6224,plain,(
% 11.14/1.88 c=divide(identity,e)|~zero=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f5307,f6221])).
% 11.14/1.88 fof(f6229,plain,(
% 11.14/1.88 c=divide(identity,e)),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f6224])).
% 11.14/1.88 fof(f6489,plain,(
% 11.14/1.88 ![X0]: (less_equal(divide(X0,b),divide(X0,g)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4477,f16])).
% 11.14/1.88 fof(f6786,plain,(
% 11.14/1.88 less_equal(d,divide(d,g))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1312,f6489])).
% 11.14/1.88 fof(f6796,plain,(
% 11.14/1.88 less_equal(d,divide(identity,g))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f23,f6489])).
% 11.14/1.88 fof(f6818,plain,(
% 11.14/1.88 d=divide(d,g)),
% 11.14/1.88 inference(resolution,[status(thm)],[f6786,f55])).
% 11.14/1.88 fof(f6846,plain,(
% 11.14/1.88 ![X0]: (divide(divide(d,g),divide(X0,g))=divide(divide(d,X0),g)|~divide(divide(divide(d,X0),g),divide(d,divide(X0,g)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6818,f141])).
% 11.14/1.88 fof(f6875,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,g))=divide(divide(d,X0),g)|~divide(divide(divide(d,X0),g),divide(d,divide(X0,g)))=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f6818,f6846])).
% 11.14/1.88 fof(f7029,plain,(
% 11.14/1.88 d=divide(identity,g)|~divide(divide(identity,g),d)=zero),
% 11.14/1.88 inference(resolution,[status(thm)],[f6796,f58])).
% 11.14/1.88 fof(f7032,plain,(
% 11.14/1.88 d=divide(identity,g)|~zero=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f5436,f7029])).
% 11.14/1.88 fof(f7037,plain,(
% 11.14/1.88 d=divide(identity,g)),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7032])).
% 11.14/1.88 fof(f7042,plain,(
% 11.14/1.88 ~less_equal(divide(d,a),divide(c,divide(g,a)))|divide(divide(identity,g),a)=divide(c,divide(g,a))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f7037,f285])).
% 11.14/1.88 fof(f7050,plain,(
% 11.14/1.88 less_equal(divide(d,divide(a,g)),divide(c,g))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f7037,f86])).
% 11.14/1.88 fof(f7087,plain,(
% 11.14/1.88 ~less_equal(divide(d,a),divide(c,divide(g,a)))|divide(d,a)=divide(c,divide(g,a))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f7037,f7042])).
% 11.14/1.88 fof(f7423,plain,(
% 11.14/1.88 ![X0,X1,X2,X3]: (zero=divide(divide(divide(X0,X1),X2),divide(X0,divide(X1,X3))))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4609,f2652])).
% 11.14/1.88 fof(f7442,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X0,divide(X1,X2)))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4609,f34])).
% 11.14/1.88 fof(f7443,plain,(
% 11.14/1.88 ![X0,X1,X2]: (less_equal(divide(X0,X1),divide(X0,divide(X1,X2))))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4609,f16])).
% 11.14/1.88 fof(f7523,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,g))=divide(divide(d,X0),g)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f7423,f6875])).
% 11.14/1.88 fof(f7524,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,b))=divide(divide(d,X0),b)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f7423,f2568])).
% 11.14/1.88 fof(f7525,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,e))=divide(divide(c,X0),e)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f7423,f6209])).
% 11.14/1.88 fof(f7526,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,a))=divide(divide(c,X0),a)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f7423,f2567])).
% 11.14/1.88 fof(f7529,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f7423,f5302])).
% 11.14/1.88 fof(f7541,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,g))=divide(divide(d,X0),g))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7523])).
% 11.14/1.88 fof(f7545,plain,(
% 11.14/1.88 ![X0]: (divide(d,divide(X0,b))=divide(divide(d,X0),b))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7524])).
% 11.14/1.88 fof(f7549,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,e))=divide(divide(c,X0),e))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7525])).
% 11.14/1.88 fof(f7553,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,a))=divide(divide(c,X0),a))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7526])).
% 11.14/1.88 fof(f7565,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(divide(X0,X1),X2),X1))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f7529])).
% 11.14/1.88 fof(f8147,plain,(
% 11.14/1.88 divide(divide(c,divide(b,a)),divide(d,a))=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f23,f494])).
% 11.14/1.88 fof(f8929,plain,(
% 11.14/1.88 divide(divide(c,divide(b,e)),divide(d,e))=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6229,f518])).
% 11.14/1.88 fof(f12647,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),divide(divide(divide(X0,X2),X1),X2)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f4609,f568])).
% 11.14/1.88 fof(f13029,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1)|~zero=zero)),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f13030,f141])).
% 11.14/1.88 fof(f13030,plain,(
% 11.14/1.88 ![X0,X1,X2]: (zero=divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2))))),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f7565,f12647])).
% 11.14/1.88 fof(f13799,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X2),X1))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f13029])).
% 11.14/1.88 fof(f18758,plain,(
% 11.14/1.88 divide(d,divide(e,b))=divide(divide(identity,e),b)|~divide(divide(c,b),divide(d,divide(e,b)))=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6229,f1023])).
% 11.14/1.88 fof(f18762,plain,(
% 11.14/1.88 divide(d,divide(a,b))=divide(divide(identity,a),b)|~divide(divide(c,b),divide(d,divide(a,b)))=zero),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f22,f1023])).
% 11.14/1.88 fof(f18807,plain,(
% 11.14/1.88 divide(d,divide(e,b))=divide(c,b)|~divide(divide(c,b),divide(d,divide(e,b)))=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f6229,f18758])).
% 11.14/1.88 fof(f18813,plain,(
% 11.14/1.88 divide(d,divide(a,b))=divide(c,b)|~divide(divide(c,b),divide(d,divide(a,b)))=zero),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f22,f18762])).
% 11.14/1.88 fof(f22026,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1))=zero)),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f13799,f7442])).
% 11.14/1.88 fof(f22027,plain,(
% 11.14/1.88 ![X0,X1,X2]: (less_equal(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1)))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f13799,f7443])).
% 11.14/1.88 fof(f24861,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(divide(X0,X2),X1)|~divide(divide(divide(X0,X2),X1),divide(divide(X0,X1),X2))=zero)),
% 11.14/1.88 inference(resolution,[status(thm)],[f22027,f58])).
% 11.14/1.88 fof(f25168,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(divide(X0,X2),X1)|~zero=zero)),
% 11.14/1.88 inference(forward_demodulation,[status(thm)],[f22026,f24861])).
% 11.14/1.88 fof(f25169,plain,(
% 11.14/1.88 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(divide(X0,X2),X1))),
% 11.14/1.88 inference(trivial_equality_resolution,[status(thm)],[f25168])).
% 11.14/1.88 fof(f25729,plain,(
% 11.14/1.88 ![X0]: (divide(c,X0)=divide(divide(c,X0),e))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6152,f25169])).
% 11.14/1.88 fof(f25730,plain,(
% 11.14/1.88 ![X0]: (divide(c,X0)=divide(divide(c,X0),a))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1550,f25169])).
% 11.14/1.88 fof(f25737,plain,(
% 11.14/1.88 ![X0]: (divide(d,X0)=divide(divide(d,X0),g))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f6818,f25169])).
% 11.14/1.88 fof(f25738,plain,(
% 11.14/1.88 ![X0]: (divide(d,X0)=divide(divide(d,X0),b))),
% 11.14/1.88 inference(paramodulation,[status(thm)],[f1312,f25169])).
% 11.14/1.88 fof(f26347,plain,(
% 11.14/1.88 ![X0]: (divide(c,divide(X0,e))=divide(c,X0))),
% 11.14/1.88 inference(backward_demodulation,[status(thm)],[f25729,f7549])).
% 5.40/1.92 fof(f26348,plain,(
% 5.40/1.92 ![X0]: (divide(c,divide(X0,a))=divide(c,X0))),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f25730,f7553])).
% 5.40/1.92 fof(f26355,plain,(
% 5.40/1.92 ![X0]: (divide(d,divide(X0,g))=divide(d,X0))),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f25737,f7541])).
% 5.40/1.92 fof(f26356,plain,(
% 5.40/1.92 ![X0]: (divide(d,divide(X0,b))=divide(d,X0))),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f25738,f7545])).
% 5.40/1.92 fof(f26689,plain,(
% 5.40/1.92 divide(divide(c,b),divide(d,e))=zero),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26347,f8929])).
% 5.40/1.92 fof(f26705,plain,(
% 5.40/1.92 ~less_equal(divide(d,a),divide(c,divide(g,a)))|divide(d,a)=divide(c,g)),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26348,f7087])).
% 5.40/1.92 fof(f26707,plain,(
% 5.40/1.92 divide(divide(c,b),divide(d,a))=zero),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26348,f8147])).
% 5.40/1.92 fof(f26725,plain,(
% 5.40/1.92 less_equal(divide(d,a),divide(c,g))),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26355,f7050])).
% 5.40/1.92 fof(f26737,plain,(
% 5.40/1.92 divide(d,divide(e,b))=divide(c,b)|~divide(divide(c,b),divide(d,e))=zero),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26356,f18807])).
% 5.40/1.92 fof(f26741,plain,(
% 5.40/1.92 divide(d,divide(a,b))=divide(c,b)|~divide(divide(c,b),divide(d,a))=zero),
% 5.40/1.92 inference(backward_demodulation,[status(thm)],[f26356,f18813])).
% 5.40/1.92 fof(f26878,plain,(
% 5.40/1.92 ~less_equal(divide(d,a),divide(c,g))|divide(d,a)=divide(c,g)),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26348,f26705])).
% 5.40/1.92 fof(f26888,plain,(
% 5.40/1.92 divide(d,a)=divide(c,g)),
% 5.40/1.92 inference(backward_subsumption_resolution,[status(thm)],[f26878,f26725])).
% 5.40/1.92 fof(f26900,plain,(
% 5.40/1.92 divide(d,e)=divide(c,b)|~divide(divide(c,b),divide(d,e))=zero),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26356,f26737])).
% 5.40/1.92 fof(f26901,plain,(
% 5.40/1.92 divide(d,e)=divide(c,b)|~zero=zero),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26689,f26900])).
% 5.40/1.92 fof(f26911,plain,(
% 5.40/1.92 divide(d,e)=divide(c,b)),
% 5.40/1.92 inference(trivial_equality_resolution,[status(thm)],[f26901])).
% 5.40/1.92 fof(f26918,plain,(
% 5.40/1.92 divide(d,a)=divide(c,b)|~divide(divide(c,b),divide(d,a))=zero),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26356,f26741])).
% 5.40/1.92 fof(f26919,plain,(
% 5.40/1.92 divide(d,a)=divide(d,e)|~divide(divide(c,b),divide(d,a))=zero),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26911,f26918])).
% 5.40/1.92 fof(f26920,plain,(
% 5.40/1.92 divide(d,a)=divide(d,e)|~zero=zero),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26707,f26919])).
% 5.40/1.92 fof(f26924,plain,(
% 5.40/1.92 divide(d,a)=divide(d,e)),
% 5.40/1.92 inference(trivial_equality_resolution,[status(thm)],[f26920])).
% 5.40/1.92 fof(f27037,plain,(
% 5.40/1.92 divide(d,e)=divide(c,g)),
% 5.40/1.92 inference(forward_demodulation,[status(thm)],[f26924,f26888])).
% 5.40/1.92 fof(f27038,plain,(
% 5.40/1.92 $false),
% 5.40/1.92 inference(forward_subsumption_resolution,[status(thm)],[f27037,f26])).
% 5.40/1.92 % SZS output end CNFRefutation for theBenchmark.p
% 5.40/1.94 % Elapsed time: 1.572173 seconds
% 5.40/1.94 % CPU time: 12.091010 seconds
% 5.40/1.94 % Total memory used: 285.962 MB
% 5.40/1.94 % Net memory used: 279.364 MB
%------------------------------------------------------------------------------