%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:23 PM UTC 2026
% Result : Unsatisfiable 21.48s 3.18s
% Output : CNFRefutation 21.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 16
% Syntax : Number of formulae : 230 ( 131 unt; 0 def)
% Number of atoms : 415 ( 61 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 373 ( 188 ~; 185 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 322 ( 322 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( quotient(X,Y,zero)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( less_equal(X,Y)
| ~ quotient(X,Y,zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] :
( less_equal(Z,X)
| ~ quotient(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,V1,Z,V2,V3,V4,V5] :
( less_equal(V4,V5)
| ~ quotient(V1,Z,V5)
| ~ quotient(V3,V2,V4)
| ~ quotient(X,Z,V3)
| ~ quotient(Y,Z,V2)
| ~ quotient(X,Y,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : less_equal(zero,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : less_equal(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : quotient(X,Y,divide(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z,W] :
( Z = W
| ~ quotient(X,Y,W)
| ~ quotient(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
quotient(identity,a,idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
quotient(identity,b,idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
quotient(identity,idQb,idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,plain,
! [X0,X1] :
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f18,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(X0,X1,zero) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f19,plain,
! [X,Z] :
( less_equal(Z,X)
| ! [Y] : ~ quotient(X,Y,Z) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f20,plain,
! [X0,X1,X2] :
( less_equal(X2,X0)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [V4,V5] :
( less_equal(V4,V5)
| ! [V1,Z] :
( ~ quotient(V1,Z,V5)
| ! [V2,V3] :
( ~ quotient(V3,V2,V4)
| ! [X] :
( ~ quotient(X,Z,V3)
| ! [Y] :
( ~ quotient(Y,Z,V2)
| ~ quotient(X,Y,V1) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f22,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( less_equal(X6,X7)
| ~ quotient(X2,X3,X7)
| ~ quotient(X5,X4,X6)
| ~ quotient(X0,X3,X5)
| ~ quotient(X1,X3,X4)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f23,plain,
! [X0] : less_equal(zero,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f24,plain,
! [X0,X1] :
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0] : less_equal(X0,identity),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0,X1] : quotient(X0,X1,divide(X0,X1)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
! [Z,W] :
( Z = W
| ! [X,Y] :
( ~ quotient(X,Y,W)
| ~ quotient(X,Y,Z) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
quotient(identity,a,idQa),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
quotient(identity,b,idQb),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
quotient(identity,idQb,idQ_idQb),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f32,plain,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f33,plain,
quotient(identity,idQa,idQ_idQa),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f34,plain,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f35,plain,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f36,plain,
! [X0] : quotient(zero,X0,zero),
inference(resolution,[status(thm)],[f17,f23]) ).
fof(f37,plain,
! [X0] : quotient(X0,identity,zero),
inference(resolution,[status(thm)],[f25,f17]) ).
fof(f48,plain,
! [X0,X1] : less_equal(divide(X0,X1),X0),
inference(resolution,[status(thm)],[f20,f26]) ).
fof(f51,plain,
! [X0,X1] : quotient(divide(X0,X1),X0,zero),
inference(resolution,[status(thm)],[f48,f17]) ).
fof(f58,plain,
! [X0,X1] :
( divide(X0,X1) = X0
| ~ less_equal(X0,divide(X0,X1)) ),
inference(resolution,[status(thm)],[f24,f48]) ).
fof(f61,plain,
! [X0] :
( zero = X0
| ~ less_equal(X0,zero) ),
inference(resolution,[status(thm)],[f24,f23]) ).
fof(f63,plain,
! [X0] : zero = divide(zero,X0),
inference(resolution,[status(thm)],[f61,f48]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X3,X4)
| ~ quotient(idQ_idQa,X0,X4)
| ~ quotient(X2,X1,X3)
| ~ quotient(identity,X0,X2)
| ~ quotient(idQa,X0,X1) ),
inference(resolution,[status(thm)],[f22,f33]) ).
fof(f73,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X3,X4)
| ~ quotient(idQ_idQb,X0,X4)
| ~ quotient(X2,X1,X3)
| ~ quotient(identity,X0,X2)
| ~ quotient(idQb,X0,X1) ),
inference(resolution,[status(thm)],[f22,f31]) ).
fof(f74,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X3,X4)
| ~ quotient(idQb,X0,X4)
| ~ quotient(X2,X1,X3)
| ~ quotient(identity,X0,X2)
| ~ quotient(b,X0,X1) ),
inference(resolution,[status(thm)],[f22,f30]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X3,X4)
| ~ quotient(idQa,X0,X4)
| ~ quotient(X2,X1,X3)
| ~ quotient(identity,X0,X2)
| ~ quotient(a,X0,X1) ),
inference(resolution,[status(thm)],[f22,f29]) ).
fof(f80,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( less_equal(X5,X6)
| ~ quotient(divide(X3,X0),X1,X6)
| ~ quotient(X4,X2,X5)
| ~ quotient(X3,X1,X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[f22,f26]) ).
fof(f91,plain,
! [X0,X1] :
( zero = X1
| ~ quotient(X0,identity,X1) ),
inference(resolution,[status(thm)],[f28,f37]) ).
fof(f92,plain,
! [X0,X1,X2] :
( divide(X0,X1) = X2
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[f28,f26]) ).
fof(f93,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(idQ_idQa,idQ_idQb,X2)
| ~ quotient(X0,idQa_Q__idQ_idQb,X1)
| ~ quotient(identity,idQ_idQb,X0) ),
inference(resolution,[status(thm)],[f72,f32]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(idQ_idQa,X0,X3)
| ~ quotient(X1,divide(idQa,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f72,f26]) ).
fof(f118,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(idQ_idQa,idQ_idQb,X1)
| ~ quotient(divide(identity,idQ_idQb),idQa_Q__idQ_idQb,X0) ),
inference(resolution,[status(thm)],[f93,f26]) ).
fof(f119,plain,
! [X0] :
( less_equal(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),X0)
| ~ quotient(idQ_idQa,idQ_idQb,X0) ),
inference(resolution,[status(thm)],[f118,f26]) ).
fof(f120,plain,
less_equal(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb)),
inference(resolution,[status(thm)],[f119,f26]) ).
fof(f122,plain,
quotient(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb),zero),
inference(resolution,[status(thm)],[f120,f17]) ).
fof(f133,plain,
! [X0] : zero = divide(X0,identity),
inference(resolution,[status(thm)],[f91,f26]) ).
fof(f171,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(idQ_idQb,idQ_idQa,X2)
| ~ quotient(X0,idQb_Q__idQ_idQa,X1)
| ~ quotient(identity,idQ_idQa,X0) ),
inference(resolution,[status(thm)],[f73,f34]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(idQ_idQb,X0,X3)
| ~ quotient(X1,divide(idQb,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f73,f26]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(idQb,X0,X3)
| ~ quotient(X1,divide(b,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f74,f26]) ).
fof(f177,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(idQa,X0,X3)
| ~ quotient(X1,divide(a,X0),X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f75,f26]) ).
fof(f182,plain,
divide(divide(divide(identity,idQ_idQb),idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb)) = zero,
inference(resolution,[status(thm)],[f122,f92]) ).
fof(f330,plain,
! [X0,X1,X2,X3,X4,X5] :
( less_equal(X3,X5)
| ~ quotient(divide(X0,divide(X1,X4)),X1,X5)
| ~ quotient(X2,zero,X3)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[f80,f51]) ).
fof(f333,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(divide(X0,identity),idQa,X3)
| ~ quotient(X1,idQ_idQa,X2)
| ~ quotient(X0,idQa,X1) ),
inference(resolution,[status(thm)],[f80,f33]) ).
fof(f334,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(divide(X0,identity),idQb,X3)
| ~ quotient(X1,idQ_idQb,X2)
| ~ quotient(X0,idQb,X1) ),
inference(resolution,[status(thm)],[f80,f31]) ).
fof(f335,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(divide(X0,identity),b,X3)
| ~ quotient(X1,idQb,X2)
| ~ quotient(X0,b,X1) ),
inference(resolution,[status(thm)],[f80,f30]) ).
fof(f336,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(divide(X0,identity),a,X3)
| ~ quotient(X1,idQa,X2)
| ~ quotient(X0,a,X1) ),
inference(resolution,[status(thm)],[f80,f29]) ).
fof(f337,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X3,X4)
| ~ quotient(divide(X0,zero),X1,X4)
| ~ quotient(X2,zero,X3)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[f80,f36]) ).
fof(f341,plain,
! [X0,X1,X2,X3,X4,X5] :
( less_equal(X4,X5)
| ~ quotient(divide(X0,X3),X1,X5)
| ~ quotient(X2,divide(X3,X1),X4)
| ~ quotient(X0,X1,X2) ),
inference(resolution,[status(thm)],[f80,f26]) ).
fof(f342,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(zero,idQa,X3)
| ~ quotient(X1,idQ_idQa,X2)
| ~ quotient(X0,idQa,X1) ),
inference(forward_demodulation,[status(thm)],[f133,f333]) ).
fof(f343,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(zero,idQb,X3)
| ~ quotient(X1,idQ_idQb,X2)
| ~ quotient(X0,idQb,X1) ),
inference(forward_demodulation,[status(thm)],[f133,f334]) ).
fof(f344,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(zero,b,X3)
| ~ quotient(X1,idQb,X2)
| ~ quotient(X0,b,X1) ),
inference(forward_demodulation,[status(thm)],[f133,f335]) ).
fof(f345,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(zero,a,X3)
| ~ quotient(X1,idQa,X2)
| ~ quotient(X0,a,X1) ),
inference(forward_demodulation,[status(thm)],[f133,f336]) ).
fof(f413,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(idQ_idQb,idQ_idQa,X1)
| ~ quotient(divide(identity,idQ_idQa),idQb_Q__idQ_idQa,X0) ),
inference(resolution,[status(thm)],[f171,f26]) ).
fof(f546,plain,
! [X0,X1,X2] :
( less_equal(divide(X1,divide(idQa,X0)),X2)
| ~ quotient(idQ_idQa,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f95,f26]) ).
fof(f552,plain,
! [X0] :
( less_equal(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),X0)
| ~ quotient(idQ_idQb,idQ_idQa,X0) ),
inference(resolution,[status(thm)],[f413,f26]) ).
fof(f553,plain,
less_equal(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa)),
inference(resolution,[status(thm)],[f552,f26]) ).
fof(f555,plain,
quotient(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa),zero),
inference(resolution,[status(thm)],[f553,f17]) ).
fof(f560,plain,
divide(divide(divide(identity,idQ_idQa),idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa)) = zero,
inference(resolution,[status(thm)],[f555,f92]) ).
fof(f633,plain,
! [X0,X1,X2] :
( less_equal(divide(X1,divide(idQb,X0)),X2)
| ~ quotient(idQ_idQb,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f173,f26]) ).
fof(f641,plain,
! [X0,X1,X2] :
( less_equal(divide(X1,divide(b,X0)),X2)
| ~ quotient(idQb,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f175,f26]) ).
fof(f702,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(zero,idQa,X1)
| ~ quotient(idQ_idQa,idQ_idQa,X0) ),
inference(resolution,[status(thm)],[f342,f33]) ).
fof(f704,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(zero,idQa,X2)
| ~ quotient(divide(X0,idQa),idQ_idQa,X1) ),
inference(resolution,[status(thm)],[f342,f26]) ).
fof(f708,plain,
! [X0] :
( less_equal(divide(idQ_idQa,idQ_idQa),X0)
| ~ quotient(zero,idQa,X0) ),
inference(resolution,[status(thm)],[f702,f26]) ).
fof(f709,plain,
less_equal(divide(idQ_idQa,idQ_idQa),zero),
inference(resolution,[status(thm)],[f708,f36]) ).
fof(f712,plain,
zero = divide(idQ_idQa,idQ_idQa),
inference(resolution,[status(thm)],[f709,f61]) ).
fof(f732,plain,
quotient(idQ_idQa,idQ_idQa,zero),
inference(paramodulation,[status(thm)],[f712,f26]) ).
fof(f742,plain,
! [X0,X1,X2] :
( less_equal(divide(X1,divide(a,X0)),X2)
| ~ quotient(idQa,X0,X2)
| ~ quotient(identity,X0,X1) ),
inference(resolution,[status(thm)],[f177,f26]) ).
fof(f746,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(zero,idQb,X1)
| ~ quotient(idQ_idQb,idQ_idQb,X0) ),
inference(resolution,[status(thm)],[f343,f31]) ).
fof(f748,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(zero,idQb,X2)
| ~ quotient(divide(X0,idQb),idQ_idQb,X1) ),
inference(resolution,[status(thm)],[f343,f26]) ).
fof(f799,plain,
! [X0] :
( less_equal(divide(idQ_idQb,idQ_idQb),X0)
| ~ quotient(zero,idQb,X0) ),
inference(resolution,[status(thm)],[f746,f26]) ).
fof(f800,plain,
less_equal(divide(idQ_idQb,idQ_idQb),zero),
inference(resolution,[status(thm)],[f799,f36]) ).
fof(f804,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(zero,b,X1)
| ~ quotient(idQb,idQb,X0) ),
inference(resolution,[status(thm)],[f344,f30]) ).
fof(f806,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(zero,b,X2)
| ~ quotient(divide(X0,b),idQb,X1) ),
inference(resolution,[status(thm)],[f344,f26]) ).
fof(f808,plain,
! [X0,X1] :
( less_equal(X0,X1)
| ~ quotient(zero,a,X1)
| ~ quotient(idQa,idQa,X0) ),
inference(resolution,[status(thm)],[f345,f29]) ).
fof(f810,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(zero,a,X2)
| ~ quotient(divide(X0,a),idQa,X1) ),
inference(resolution,[status(thm)],[f345,f26]) ).
fof(f835,plain,
! [X0,X1,X2,X3] :
( less_equal(X2,X3)
| ~ quotient(divide(X0,zero),X1,X3)
| ~ quotient(divide(X0,X1),zero,X2) ),
inference(resolution,[status(thm)],[f337,f26]) ).
fof(f895,plain,
zero = divide(idQ_idQb,idQ_idQb),
inference(resolution,[status(thm)],[f800,f61]) ).
fof(f916,plain,
quotient(idQ_idQb,idQ_idQb,zero),
inference(paramodulation,[status(thm)],[f895,f26]) ).
fof(f985,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(divide(idQb,X0),idQ_idQa,X2)
| ~ quotient(idQb_Q__idQ_idQa,divide(X0,idQ_idQa),X1) ),
inference(resolution,[status(thm)],[f341,f34]) ).
fof(f986,plain,
! [X0,X1,X2] :
( less_equal(X1,X2)
| ~ quotient(divide(idQa,X0),idQ_idQb,X2)
| ~ quotient(idQa_Q__idQ_idQb,divide(X0,idQ_idQb),X1) ),
inference(resolution,[status(thm)],[f341,f32]) ).
fof(f1108,plain,
! [X0,X1] :
( less_equal(divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)),X1)
| ~ quotient(divide(idQb,X0),idQ_idQa,X1) ),
inference(resolution,[status(thm)],[f985,f26]) ).
fof(f1142,plain,
! [X0] :
( less_equal(divide(idQb,idQb),X0)
| ~ quotient(zero,b,X0) ),
inference(resolution,[status(thm)],[f804,f26]) ).
fof(f1143,plain,
less_equal(divide(idQb,idQb),zero),
inference(resolution,[status(thm)],[f1142,f36]) ).
fof(f1146,plain,
zero = divide(idQb,idQb),
inference(resolution,[status(thm)],[f1143,f61]) ).
fof(f1178,plain,
quotient(idQb,idQb,zero),
inference(paramodulation,[status(thm)],[f1146,f26]) ).
fof(f1234,plain,
! [X0,X1,X2] :
( less_equal(X0,X2)
| ~ quotient(divide(identity,divide(b,X1)),b,X2)
| ~ quotient(idQb,zero,X0) ),
inference(resolution,[status(thm)],[f330,f30]) ).
fof(f1235,plain,
! [X0,X1,X2] :
( less_equal(X0,X2)
| ~ quotient(divide(identity,divide(a,X1)),a,X2)
| ~ quotient(idQa,zero,X0) ),
inference(resolution,[status(thm)],[f330,f29]) ).
fof(f1241,plain,
! [X0,X1,X2,X3,X4] :
( less_equal(X2,X4)
| ~ quotient(divide(X0,divide(X1,X3)),X1,X4)
| ~ quotient(divide(X0,X1),zero,X2) ),
inference(resolution,[status(thm)],[f330,f26]) ).
fof(f1271,plain,
! [X0,X1] :
( less_equal(divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)),X1)
| ~ quotient(divide(idQa,X0),idQ_idQb,X1) ),
inference(resolution,[status(thm)],[f986,f26]) ).
fof(f1301,plain,
! [X0] :
( less_equal(divide(idQa,idQa),X0)
| ~ quotient(zero,a,X0) ),
inference(resolution,[status(thm)],[f808,f26]) ).
fof(f1302,plain,
less_equal(divide(idQa,idQa),zero),
inference(resolution,[status(thm)],[f1301,f36]) ).
fof(f1305,plain,
zero = divide(idQa,idQa),
inference(resolution,[status(thm)],[f1302,f61]) ).
fof(f1331,plain,
quotient(idQa,idQa,zero),
inference(paramodulation,[status(thm)],[f1305,f26]) ).
fof(f1585,plain,
! [X0,X1] :
( less_equal(divide(divide(X1,idQa),idQ_idQa),X0)
| ~ quotient(zero,idQa,X0) ),
inference(resolution,[status(thm)],[f704,f26]) ).
fof(f1591,plain,
! [X0] : less_equal(divide(divide(X0,idQa),idQ_idQa),zero),
inference(resolution,[status(thm)],[f1585,f36]) ).
fof(f1594,plain,
! [X0] : zero = divide(divide(X0,idQa),idQ_idQa),
inference(resolution,[status(thm)],[f1591,f61]) ).
fof(f1632,plain,
! [X0] : quotient(divide(X0,idQa),idQ_idQa,zero),
inference(paramodulation,[status(thm)],[f1594,f26]) ).
fof(f1778,plain,
! [X0] : less_equal(divide(X0,idQa),idQ_idQa),
inference(resolution,[status(thm)],[f1632,f18]) ).
fof(f1794,plain,
! [X0] :
( divide(X0,idQa) = idQ_idQa
| ~ less_equal(idQ_idQa,divide(X0,idQa)) ),
inference(resolution,[status(thm)],[f1778,f24]) ).
fof(f1821,plain,
! [X0,X1] :
( less_equal(divide(divide(X1,idQb),idQ_idQb),X0)
| ~ quotient(zero,idQb,X0) ),
inference(resolution,[status(thm)],[f748,f26]) ).
fof(f1827,plain,
! [X0] : less_equal(divide(divide(X0,idQb),idQ_idQb),zero),
inference(resolution,[status(thm)],[f1821,f36]) ).
fof(f1830,plain,
! [X0] : zero = divide(divide(X0,idQb),idQ_idQb),
inference(resolution,[status(thm)],[f1827,f61]) ).
fof(f1868,plain,
! [X0] : quotient(divide(X0,idQb),idQ_idQb,zero),
inference(paramodulation,[status(thm)],[f1830,f26]) ).
fof(f1918,plain,
! [X0,X1] :
( less_equal(divide(divide(identity,X0),divide(idQa,X0)),X1)
| ~ quotient(idQ_idQa,X0,X1) ),
inference(resolution,[status(thm)],[f546,f26]) ).
fof(f1926,plain,
! [X0,X1] :
( less_equal(divide(divide(identity,X0),divide(idQb,X0)),X1)
| ~ quotient(idQ_idQb,X0,X1) ),
inference(resolution,[status(thm)],[f633,f26]) ).
fof(f1982,plain,
! [X0] : less_equal(divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)),divide(divide(idQb,X0),idQ_idQa)),
inference(resolution,[status(thm)],[f1108,f26]) ).
fof(f2038,plain,
! [X0] :
( divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa)) = divide(divide(idQb,X0),idQ_idQa)
| ~ less_equal(divide(divide(idQb,X0),idQ_idQa),divide(idQb_Q__idQ_idQa,divide(X0,idQ_idQa))) ),
inference(resolution,[status(thm)],[f1982,f24]) ).
fof(f2073,plain,
! [X0] : less_equal(divide(X0,idQb),idQ_idQb),
inference(resolution,[status(thm)],[f1868,f18]) ).
fof(f2090,plain,
! [X0] :
( divide(X0,idQb) = idQ_idQb
| ~ less_equal(idQ_idQb,divide(X0,idQb)) ),
inference(resolution,[status(thm)],[f2073,f24]) ).
fof(f2150,plain,
! [X0] :
( less_equal(divide(idQ_idQb,divide(b,idQb)),X0)
| ~ quotient(idQb,idQb,X0) ),
inference(resolution,[status(thm)],[f641,f31]) ).
fof(f2156,plain,
! [X0] :
( less_equal(divide(idQ_idQa,divide(a,idQa)),X0)
| ~ quotient(idQa,idQa,X0) ),
inference(resolution,[status(thm)],[f742,f33]) ).
fof(f2164,plain,
! [X0,X1] :
( less_equal(divide(divide(X1,b),idQb),X0)
| ~ quotient(zero,b,X0) ),
inference(resolution,[status(thm)],[f806,f26]) ).
fof(f2194,plain,
! [X0] : less_equal(divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)),divide(divide(idQa,X0),idQ_idQb)),
inference(resolution,[status(thm)],[f1271,f26]) ).
fof(f2310,plain,
! [X0,X1] :
( less_equal(divide(divide(X1,a),idQa),X0)
| ~ quotient(zero,a,X0) ),
inference(resolution,[status(thm)],[f810,f26]) ).
fof(f2318,plain,
! [X0] :
( divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb)) = divide(divide(idQa,X0),idQ_idQb)
| ~ less_equal(divide(divide(idQa,X0),idQ_idQb),divide(idQa_Q__idQ_idQb,divide(X0,idQ_idQb))) ),
inference(resolution,[status(thm)],[f2194,f24]) ).
fof(f2404,plain,
! [X0] : less_equal(divide(divide(X0,b),idQb),zero),
inference(resolution,[status(thm)],[f2164,f36]) ).
fof(f2407,plain,
! [X0] : zero = divide(divide(X0,b),idQb),
inference(resolution,[status(thm)],[f2404,f61]) ).
fof(f2444,plain,
! [X0] : quotient(divide(X0,b),idQb,zero),
inference(paramodulation,[status(thm)],[f2407,f26]) ).
fof(f2454,plain,
! [X0] : less_equal(divide(X0,b),idQb),
inference(resolution,[status(thm)],[f2444,f18]) ).
fof(f2470,plain,
! [X0] :
( divide(X0,b) = idQb
| ~ less_equal(idQb,divide(X0,b)) ),
inference(resolution,[status(thm)],[f2454,f24]) ).
fof(f2588,plain,
! [X0] : less_equal(divide(divide(X0,a),idQa),zero),
inference(resolution,[status(thm)],[f2310,f36]) ).
fof(f2591,plain,
! [X0] : zero = divide(divide(X0,a),idQa),
inference(resolution,[status(thm)],[f2588,f61]) ).
fof(f2627,plain,
! [X0] : quotient(divide(X0,a),idQa,zero),
inference(paramodulation,[status(thm)],[f2591,f26]) ).
fof(f2636,plain,
! [X0] : less_equal(divide(X0,a),idQa),
inference(resolution,[status(thm)],[f2627,f18]) ).
fof(f2652,plain,
! [X0] :
( divide(X0,a) = idQa
| ~ less_equal(idQa,divide(X0,a)) ),
inference(resolution,[status(thm)],[f2636,f24]) ).
fof(f2709,plain,
! [X0,X1,X2] :
( less_equal(divide(divide(X0,X1),zero),X2)
| ~ quotient(divide(X0,zero),X1,X2) ),
inference(resolution,[status(thm)],[f835,f26]) ).
fof(f4834,plain,
less_equal(divide(idQ_idQb,divide(b,idQb)),zero),
inference(resolution,[status(thm)],[f2150,f1178]) ).
fof(f4837,plain,
zero = divide(idQ_idQb,divide(b,idQb)),
inference(resolution,[status(thm)],[f4834,f61]) ).
fof(f4862,plain,
quotient(idQ_idQb,divide(b,idQb),zero),
inference(paramodulation,[status(thm)],[f4837,f26]) ).
fof(f4869,plain,
less_equal(idQ_idQb,divide(b,idQb)),
inference(resolution,[status(thm)],[f4862,f18]) ).
fof(f4882,plain,
divide(b,idQb) = idQ_idQb,
inference(resolution,[status(thm)],[f4869,f2090]) ).
fof(f4923,plain,
! [X0,X1] :
( less_equal(divide(idQb,zero),X1)
| ~ quotient(divide(identity,divide(b,X0)),b,X1) ),
inference(resolution,[status(thm)],[f1234,f26]) ).
fof(f4924,plain,
! [X0,X1] :
( less_equal(divide(idQa,zero),X1)
| ~ quotient(divide(identity,divide(a,X0)),a,X1) ),
inference(resolution,[status(thm)],[f1235,f26]) ).
fof(f5177,plain,
! [X0,X1,X2,X3] :
( less_equal(divide(divide(X0,X1),zero),X3)
| ~ quotient(divide(X0,divide(X1,X2)),X1,X3) ),
inference(resolution,[status(thm)],[f1241,f26]) ).
fof(f5656,plain,
less_equal(divide(divide(identity,idQ_idQa),divide(idQa,idQ_idQa)),zero),
inference(resolution,[status(thm)],[f1918,f732]) ).
fof(f5662,plain,
less_equal(divide(divide(identity,idQ_idQb),divide(idQb,idQ_idQb)),zero),
inference(resolution,[status(thm)],[f1926,f916]) ).
fof(f5802,plain,
zero = divide(divide(identity,idQ_idQa),divide(idQa,idQ_idQa)),
inference(resolution,[status(thm)],[f5656,f61]) ).
fof(f5846,plain,
zero = divide(divide(identity,idQ_idQb),divide(idQb,idQ_idQb)),
inference(resolution,[status(thm)],[f5662,f61]) ).
fof(f5882,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(resolution,[status(thm)],[f2156,f1331]) ).
fof(f6137,plain,
zero = divide(idQ_idQa,divide(a,idQa)),
inference(resolution,[status(thm)],[f5882,f61]) ).
fof(f6165,plain,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(paramodulation,[status(thm)],[f6137,f26]) ).
fof(f6174,plain,
less_equal(idQ_idQa,divide(a,idQa)),
inference(resolution,[status(thm)],[f6165,f18]) ).
fof(f6187,plain,
divide(a,idQa) = idQ_idQa,
inference(resolution,[status(thm)],[f6174,f1794]) ).
fof(f7193,plain,
! [X0] : less_equal(divide(divide(X0,X0),zero),zero),
inference(resolution,[status(thm)],[f2709,f51]) ).
fof(f7483,plain,
! [X0] : zero = divide(divide(X0,X0),zero),
inference(resolution,[status(thm)],[f7193,f61]) ).
fof(f7534,plain,
! [X0] : quotient(divide(X0,X0),zero,zero),
inference(paramodulation,[status(thm)],[f7483,f26]) ).
fof(f7552,plain,
! [X0] : less_equal(divide(X0,X0),zero),
inference(resolution,[status(thm)],[f7534,f18]) ).
fof(f7576,plain,
! [X0] : zero = divide(X0,X0),
inference(resolution,[status(thm)],[f7552,f61]) ).
fof(f7806,plain,
! [X0] : quotient(X0,X0,zero),
inference(paramodulation,[status(thm)],[f7576,f26]) ).
fof(f8241,plain,
! [X0] : less_equal(divide(divide(X0,divide(X0,zero)),zero),zero),
inference(resolution,[status(thm)],[f7806,f2709]) ).
fof(f8378,plain,
! [X0] : zero = divide(divide(X0,divide(X0,zero)),zero),
inference(resolution,[status(thm)],[f8241,f61]) ).
fof(f8680,plain,
! [X0] : quotient(divide(X0,divide(X0,zero)),zero,zero),
inference(paramodulation,[status(thm)],[f8378,f26]) ).
fof(f8695,plain,
! [X0] : less_equal(divide(X0,divide(X0,zero)),zero),
inference(resolution,[status(thm)],[f8680,f18]) ).
fof(f8719,plain,
! [X0] : zero = divide(X0,divide(X0,zero)),
inference(resolution,[status(thm)],[f8695,f61]) ).
fof(f8866,plain,
! [X0] : quotient(X0,divide(X0,zero),zero),
inference(paramodulation,[status(thm)],[f8719,f26]) ).
fof(f8987,plain,
! [X0] : less_equal(X0,divide(X0,zero)),
inference(resolution,[status(thm)],[f8866,f18]) ).
fof(f9017,plain,
! [X0] : divide(X0,zero) = X0,
inference(resolution,[status(thm)],[f8987,f58]) ).
fof(f12629,plain,
! [X0,X1] :
( less_equal(idQb,X1)
| ~ quotient(divide(identity,divide(b,X0)),b,X1) ),
inference(forward_demodulation,[status(thm)],[f9017,f4923]) ).
fof(f12631,plain,
! [X0] :
( less_equal(idQb,X0)
| ~ quotient(divide(identity,idQ_idQb),b,X0) ),
inference(paramodulation,[status(thm)],[f4882,f12629]) ).
fof(f12638,plain,
! [X0,X1] :
( less_equal(idQa,X1)
| ~ quotient(divide(identity,divide(a,X0)),a,X1) ),
inference(forward_demodulation,[status(thm)],[f9017,f4924]) ).
fof(f12640,plain,
! [X0] :
( less_equal(idQa,X0)
| ~ quotient(divide(identity,idQ_idQa),a,X0) ),
inference(paramodulation,[status(thm)],[f6187,f12638]) ).
fof(f12647,plain,
! [X0,X1,X2,X3] :
( less_equal(divide(X0,X1),X3)
| ~ quotient(divide(X0,divide(X1,X2)),X1,X3) ),
inference(forward_demodulation,[status(thm)],[f9017,f5177]) ).
fof(f12655,plain,
! [X0,X1,X2] : less_equal(divide(X0,X1),divide(divide(X0,divide(X1,X2)),X1)),
inference(resolution,[status(thm)],[f12647,f26]) ).
fof(f17191,plain,
less_equal(idQb,divide(divide(identity,idQ_idQb),b)),
inference(resolution,[status(thm)],[f12631,f26]) ).
fof(f17192,plain,
divide(divide(identity,idQ_idQb),b) = idQb,
inference(resolution,[status(thm)],[f17191,f2470]) ).
fof(f17239,plain,
less_equal(idQb,divide(identity,idQ_idQb)),
inference(paramodulation,[status(thm)],[f17192,f48]) ).
fof(f17828,plain,
less_equal(idQa,divide(divide(identity,idQ_idQa),a)),
inference(resolution,[status(thm)],[f12640,f26]) ).
fof(f17829,plain,
divide(divide(identity,idQ_idQa),a) = idQa,
inference(resolution,[status(thm)],[f17828,f2652]) ).
fof(f17880,plain,
less_equal(idQa,divide(identity,idQ_idQa)),
inference(paramodulation,[status(thm)],[f17829,f48]) ).
fof(f18737,plain,
less_equal(divide(divide(identity,idQ_idQb),idQb),divide(zero,idQb)),
inference(paramodulation,[status(thm)],[f5846,f12655]) ).
fof(f18738,plain,
less_equal(divide(divide(identity,idQ_idQa),idQa),divide(zero,idQa)),
inference(paramodulation,[status(thm)],[f5802,f12655]) ).
fof(f18895,plain,
less_equal(divide(divide(identity,idQ_idQb),idQb),zero),
inference(forward_demodulation,[status(thm)],[f63,f18737]) ).
fof(f18896,plain,
less_equal(divide(divide(identity,idQ_idQa),idQa),zero),
inference(forward_demodulation,[status(thm)],[f63,f18738]) ).
fof(f19715,plain,
zero = divide(divide(identity,idQ_idQb),idQb),
inference(resolution,[status(thm)],[f18895,f61]) ).
fof(f19775,plain,
quotient(divide(identity,idQ_idQb),idQb,zero),
inference(paramodulation,[status(thm)],[f19715,f26]) ).
fof(f19815,plain,
less_equal(divide(identity,idQ_idQb),idQb),
inference(resolution,[status(thm)],[f19775,f18]) ).
fof(f19836,plain,
( divide(identity,idQ_idQb) = idQb
| ~ less_equal(idQb,divide(identity,idQ_idQb)) ),
inference(resolution,[status(thm)],[f19815,f24]) ).
fof(f19838,plain,
divide(identity,idQ_idQb) = idQb,
inference(forward_subsumption_resolution,[status(thm)],[f19836,f17239]) ).
fof(f20947,plain,
divide(divide(idQb,idQa_Q__idQ_idQb),divide(idQ_idQa,idQ_idQb)) = zero,
inference(backward_demodulation,[status(thm)],[f19838,f182]) ).
fof(f22900,plain,
zero = divide(divide(identity,idQ_idQa),idQa),
inference(resolution,[status(thm)],[f18896,f61]) ).
fof(f23454,plain,
quotient(divide(identity,idQ_idQa),idQa,zero),
inference(paramodulation,[status(thm)],[f22900,f26]) ).
fof(f23837,plain,
less_equal(divide(identity,idQ_idQa),idQa),
inference(resolution,[status(thm)],[f23454,f18]) ).
fof(f23858,plain,
( divide(identity,idQ_idQa) = idQa
| ~ less_equal(idQa,divide(identity,idQ_idQa)) ),
inference(resolution,[status(thm)],[f23837,f24]) ).
fof(f23860,plain,
divide(identity,idQ_idQa) = idQa,
inference(forward_subsumption_resolution,[status(thm)],[f23858,f17880]) ).
fof(f23894,plain,
divide(divide(idQa,idQb_Q__idQ_idQa),divide(idQ_idQb,idQ_idQa)) = zero,
inference(backward_demodulation,[status(thm)],[f23860,f560]) ).
fof(f25009,plain,
less_equal(divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa),divide(zero,idQ_idQa)),
inference(paramodulation,[status(thm)],[f20947,f12655]) ).
fof(f25047,plain,
less_equal(divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa),zero),
inference(forward_demodulation,[status(thm)],[f63,f25009]) ).
fof(f26353,plain,
zero = divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa),
inference(resolution,[status(thm)],[f25047,f61]) ).
fof(f26361,plain,
( divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)) = divide(divide(idQb,idQa_Q__idQ_idQb),idQ_idQa)
| ~ less_equal(zero,divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa))) ),
inference(paramodulation,[status(thm)],[f26353,f2038]) ).
fof(f26422,plain,
( divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)) = zero
| ~ less_equal(zero,divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa))) ),
inference(forward_demodulation,[status(thm)],[f26353,f26361]) ).
fof(f26423,plain,
divide(idQb_Q__idQ_idQa,divide(idQa_Q__idQ_idQb,idQ_idQa)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[f26422,f23]) ).
fof(f26502,plain,
less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),divide(zero,idQa_Q__idQ_idQb)),
inference(paramodulation,[status(thm)],[f26423,f12655]) ).
fof(f26557,plain,
less_equal(divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),zero),
inference(forward_demodulation,[status(thm)],[f63,f26502]) ).
fof(f26572,plain,
zero = divide(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),
inference(resolution,[status(thm)],[f26557,f61]) ).
fof(f26648,plain,
quotient(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb,zero),
inference(paramodulation,[status(thm)],[f26572,f26]) ).
fof(f26699,plain,
less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb),
inference(resolution,[status(thm)],[f26648,f18]) ).
fof(f26717,plain,
( idQb_Q__idQ_idQa = idQa_Q__idQ_idQb
| ~ less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa) ),
inference(resolution,[status(thm)],[f26699,f24]) ).
fof(f26719,plain,
~ less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(forward_subsumption_resolution,[status(thm)],[f26717,f35]) ).
fof(f36171,plain,
less_equal(divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb),divide(zero,idQ_idQb)),
inference(paramodulation,[status(thm)],[f23894,f12655]) ).
fof(f36211,plain,
less_equal(divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb),zero),
inference(forward_demodulation,[status(thm)],[f63,f36171]) ).
fof(f36229,plain,
zero = divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb),
inference(resolution,[status(thm)],[f36211,f61]) ).
fof(f36235,plain,
( divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) = divide(divide(idQa,idQb_Q__idQ_idQa),idQ_idQb)
| ~ less_equal(zero,divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb))) ),
inference(paramodulation,[status(thm)],[f36229,f2318]) ).
fof(f36304,plain,
( divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) = zero
| ~ less_equal(zero,divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb))) ),
inference(forward_demodulation,[status(thm)],[f36229,f36235]) ).
fof(f36305,plain,
divide(idQa_Q__idQ_idQb,divide(idQb_Q__idQ_idQa,idQ_idQb)) = zero,
inference(forward_subsumption_resolution,[status(thm)],[f36304,f23]) ).
fof(f36403,plain,
less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),divide(zero,idQb_Q__idQ_idQa)),
inference(paramodulation,[status(thm)],[f36305,f12655]) ).
fof(f36470,plain,
less_equal(divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),zero),
inference(forward_demodulation,[status(thm)],[f63,f36403]) ).
fof(f36488,plain,
zero = divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(resolution,[status(thm)],[f36470,f61]) ).
fof(f36576,plain,
quotient(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa,zero),
inference(paramodulation,[status(thm)],[f36488,f26]) ).
fof(f36641,plain,
less_equal(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(resolution,[status(thm)],[f36576,f18]) ).
fof(f36658,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f36641,f26719]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.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:51:38 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 21.48/3.18 % Refutation found
% 21.48/3.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.48/3.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 18.97/3.21 % Elapsed time: 2.840859 seconds
% 18.97/3.21 % CPU time: 22.271201 seconds
% 18.97/3.21 % Total memory used: 178.446 MB
% 18.97/3.21 % Net memory used: 156.430 MB
%------------------------------------------------------------------------------