%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HEN009-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:22 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.51s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 11
% Syntax : Number of formulae : 129 ( 67 unt; 0 def)
% Number of atoms : 195 ( 146 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 170 ( 104 ~; 66 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 138 ( 138 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : less_equal(divide(X,Y),X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Z,Y] : less_equal(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)),
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(f9,hypothesis,
divide(identity,a) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
divide(identity,b) = c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
divide(identity,c) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
b != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,plain,
! [X0,X1] :
( divide(X0,X1) = zero
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
! [X0,X1] :
( less_equal(X0,X1)
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f15,plain,
! [X0,X1] : less_equal(divide(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f16,plain,
! [X0,X1,X2] : less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
! [X0] : less_equal(zero,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f18,plain,
! [X0,X1] :
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f19,plain,
! [X0] : less_equal(X0,identity),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f21,plain,
divide(identity,a) = b,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
divide(identity,b) = c,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f23,plain,
divide(identity,c) = d,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f24,plain,
b != d,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f29,plain,
! [X0] : divide(zero,X0) = zero,
inference(resolution,[status(thm)],[f13,f17]) ).
fof(f30,plain,
! [X0] : divide(X0,identity) = zero,
inference(resolution,[status(thm)],[f19,f13]) ).
fof(f31,plain,
! [X0,X1] : divide(divide(X0,X1),X0) = zero,
inference(resolution,[status(thm)],[f15,f13]) ).
fof(f49,plain,
! [X0] :
( X0 = zero
| ~ less_equal(X0,zero) ),
inference(resolution,[status(thm)],[f18,f17]) ).
fof(f53,plain,
! [X0] :
( X0 = zero
| divide(X0,zero) != zero ),
inference(resolution,[status(thm)],[f14,f49]) ).
fof(f54,plain,
! [X0,X1] :
( X1 = X0
| ~ less_equal(X1,X0)
| divide(X0,X1) != zero ),
inference(resolution,[status(thm)],[f14,f18]) ).
fof(f56,plain,
! [X0,X1,X2] :
( divide(divide(X0,X1),X2) = divide(divide(X0,X2),divide(X1,X2))
| ~ less_equal(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2))) ),
inference(resolution,[status(thm)],[f16,f18]) ).
fof(f57,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = zero,
inference(resolution,[status(thm)],[f16,f13]) ).
fof(f65,plain,
! [X0,X1,X2] : less_equal(divide(divide(X0,X1),zero),divide(divide(X0,divide(X1,X2)),X1)),
inference(paramodulation,[status(thm)],[f31,f16]) ).
fof(f67,plain,
! [X0] : less_equal(divide(divide(X0,b),c),divide(divide(X0,identity),b)),
inference(paramodulation,[status(thm)],[f22,f16]) ).
fof(f69,plain,
! [X0] : less_equal(divide(divide(X0,a),b),divide(divide(X0,identity),a)),
inference(paramodulation,[status(thm)],[f21,f16]) ).
fof(f87,plain,
! [X0] : less_equal(divide(divide(X0,b),c),divide(zero,b)),
inference(forward_demodulation,[status(thm)],[f30,f67]) ).
fof(f88,plain,
! [X0] : less_equal(divide(divide(X0,b),c),zero),
inference(forward_demodulation,[status(thm)],[f29,f87]) ).
fof(f91,plain,
! [X0] : less_equal(divide(divide(X0,a),b),divide(zero,a)),
inference(forward_demodulation,[status(thm)],[f30,f69]) ).
fof(f92,plain,
! [X0] : less_equal(divide(divide(X0,a),b),zero),
inference(forward_demodulation,[status(thm)],[f29,f91]) ).
fof(f127,plain,
! [X0,X1,X2] :
( divide(divide(X0,X2),divide(X1,X2)) = divide(divide(X0,X1),X2)
| divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2))) != zero ),
inference(resolution,[status(thm)],[f54,f16]) ).
fof(f131,plain,
! [X0,X1] :
( divide(X1,X0) != zero
| X1 = X0
| divide(X0,X1) != zero ),
inference(resolution,[status(thm)],[f54,f14]) ).
fof(f132,plain,
! [X0] : divide(divide(X0,b),c) = zero,
inference(resolution,[status(thm)],[f88,f49]) ).
fof(f191,plain,
! [X0] :
( divide(divide(X0,b),c) = divide(divide(X0,c),divide(b,c))
| ~ less_equal(zero,divide(divide(X0,c),divide(b,c))) ),
inference(paramodulation,[status(thm)],[f132,f56]) ).
fof(f196,plain,
! [X0,X1,X2] :
( divide(divide(divide(X1,X2),X1),X0) = divide(divide(divide(X1,X2),X0),divide(X1,X0))
| ~ less_equal(divide(zero,X0),divide(divide(divide(X1,X2),X0),divide(X1,X0))) ),
inference(paramodulation,[status(thm)],[f31,f56]) ).
fof(f213,plain,
! [X0,X1,X2] :
( divide(divide(X0,divide(X1,X2)),X1) = divide(divide(X0,X1),divide(divide(X1,X2),X1))
| ~ less_equal(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero)) ),
inference(paramodulation,[status(thm)],[f31,f56]) ).
fof(f214,plain,
! [X0,X1] :
( divide(divide(X0,zero),X1) = divide(divide(X0,X1),divide(zero,X1))
| ~ less_equal(divide(divide(X0,zero),X1),divide(divide(X0,X1),zero)) ),
inference(paramodulation,[status(thm)],[f29,f56]) ).
fof(f219,plain,
! [X0] :
( zero = divide(divide(X0,c),divide(b,c))
| ~ less_equal(zero,divide(divide(X0,c),divide(b,c))) ),
inference(forward_demodulation,[status(thm)],[f132,f191]) ).
fof(f221,plain,
! [X0] : zero = divide(divide(X0,c),divide(b,c)),
inference(forward_subsumption_resolution,[status(thm)],[f219,f17]) ).
fof(f239,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,X1),X0),X2) = divide(divide(divide(X0,X1),X2),divide(X0,X2))
| ~ less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2))) ),
inference(forward_demodulation,[status(thm)],[f29,f196]) ).
fof(f240,plain,
! [X0,X1,X2] :
( divide(zero,X2) = divide(divide(divide(X0,X1),X2),divide(X0,X2))
| ~ less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2))) ),
inference(forward_demodulation,[status(thm)],[f31,f239]) ).
fof(f241,plain,
! [X0,X1,X2] :
( zero = divide(divide(divide(X0,X1),X2),divide(X0,X2))
| ~ less_equal(zero,divide(divide(divide(X0,X1),X2),divide(X0,X2))) ),
inference(forward_demodulation,[status(thm)],[f29,f240]) ).
fof(f243,plain,
! [X0,X1,X2] : zero = divide(divide(divide(X0,X1),X2),divide(X0,X2)),
inference(forward_subsumption_resolution,[status(thm)],[f241,f17]) ).
fof(f286,plain,
! [X0,X1,X2] :
( divide(divide(X0,divide(X1,X2)),X1) = divide(divide(X0,X1),zero)
| ~ less_equal(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero)) ),
inference(forward_demodulation,[status(thm)],[f31,f213]) ).
fof(f287,plain,
! [X0,X1] :
( divide(divide(X0,zero),X1) = divide(divide(X0,X1),zero)
| ~ less_equal(divide(divide(X0,zero),X1),divide(divide(X0,X1),zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f214]) ).
fof(f315,plain,
! [X0] : divide(divide(b,divide(X0,a)),divide(divide(identity,X0),a)) = zero,
inference(paramodulation,[status(thm)],[f21,f57]) ).
fof(f591,plain,
! [X0] : divide(divide(X0,a),b) = zero,
inference(resolution,[status(thm)],[f92,f49]) ).
fof(f611,plain,
! [X0] :
( divide(divide(X0,a),b) = divide(divide(X0,b),divide(a,b))
| ~ less_equal(zero,divide(divide(X0,b),divide(a,b))) ),
inference(paramodulation,[status(thm)],[f591,f56]) ).
fof(f631,plain,
! [X0] :
( zero = divide(divide(X0,b),divide(a,b))
| ~ less_equal(zero,divide(divide(X0,b),divide(a,b))) ),
inference(forward_demodulation,[status(thm)],[f591,f611]) ).
fof(f633,plain,
! [X0] : zero = divide(divide(X0,b),divide(a,b)),
inference(forward_subsumption_resolution,[status(thm)],[f631,f17]) ).
fof(f736,plain,
zero = divide(c,divide(a,b)),
inference(paramodulation,[status(thm)],[f22,f633]) ).
fof(f1230,plain,
zero = divide(d,divide(b,c)),
inference(paramodulation,[status(thm)],[f23,f221]) ).
fof(f1357,plain,
! [X0,X1,X2] : zero = divide(divide(divide(divide(X0,X1),X2),X0),zero),
inference(paramodulation,[status(thm)],[f31,f243]) ).
fof(f1863,plain,
less_equal(divide(divide(d,b),zero),divide(zero,b)),
inference(paramodulation,[status(thm)],[f1230,f65]) ).
fof(f1864,plain,
less_equal(divide(divide(c,a),zero),divide(zero,a)),
inference(paramodulation,[status(thm)],[f736,f65]) ).
fof(f1934,plain,
less_equal(divide(divide(d,b),zero),zero),
inference(forward_demodulation,[status(thm)],[f29,f1863]) ).
fof(f1935,plain,
less_equal(divide(divide(c,a),zero),zero),
inference(forward_demodulation,[status(thm)],[f29,f1864]) ).
fof(f2146,plain,
divide(divide(d,b),zero) = zero,
inference(resolution,[status(thm)],[f1934,f49]) ).
fof(f2154,plain,
divide(d,b) = zero,
inference(resolution,[status(thm)],[f2146,f53]) ).
fof(f2959,plain,
( divide(b,d) != zero
| divide(d,b) != zero ),
inference(resolution,[status(thm)],[f131,f24]) ).
fof(f2979,plain,
( divide(b,d) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f2154,f2959]) ).
fof(f2980,plain,
divide(b,d) != zero,
inference(trivial_equality_resolution,[status(thm)],[f2979]) ).
fof(f2995,plain,
( divide(divide(b,d),zero) != zero
| divide(zero,divide(b,d)) != zero ),
inference(resolution,[status(thm)],[f2980,f131]) ).
fof(f2997,plain,
( divide(divide(b,d),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f2995]) ).
fof(f2998,plain,
divide(divide(b,d),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f2997]) ).
fof(f3147,plain,
! [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 ),
inference(paramodulation,[status(thm)],[f31,f127]) ).
fof(f3412,plain,
! [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),zero) != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3147]) ).
fof(f3413,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,X1),X0),divide(X2,X0)) = divide(divide(divide(X0,X1),X2),X0)
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f1357,f3412]) ).
fof(f3414,plain,
! [X0,X1,X2] :
( divide(zero,divide(X0,X1)) = divide(divide(divide(X1,X2),X0),X1)
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f31,f3413]) ).
fof(f3415,plain,
! [X0,X1,X2] :
( zero = divide(divide(divide(X0,X1),X2),X0)
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3414]) ).
fof(f3417,plain,
! [X0,X1,X2] : zero = divide(divide(divide(X0,X1),X2),X0),
inference(trivial_equality_resolution,[status(thm)],[f3415]) ).
fof(f3544,plain,
( divide(divide(divide(b,d),zero),zero) != zero
| divide(zero,divide(divide(b,d),zero)) != zero ),
inference(resolution,[status(thm)],[f2998,f131]) ).
fof(f3546,plain,
( divide(divide(divide(b,d),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3544]) ).
fof(f3547,plain,
divide(divide(divide(b,d),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f3546]) ).
fof(f3550,plain,
( divide(divide(divide(divide(b,d),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(b,d),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f3547,f131]) ).
fof(f3552,plain,
( divide(divide(divide(divide(b,d),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3550]) ).
fof(f3553,plain,
divide(divide(divide(divide(b,d),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f3552]) ).
fof(f3556,plain,
( divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(b,d),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f3553,f131]) ).
fof(f3558,plain,
( divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3556]) ).
fof(f3559,plain,
divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f3558]) ).
fof(f3562,plain,
( divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f3559,f131]) ).
fof(f3564,plain,
( divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3562]) ).
fof(f3565,plain,
divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f3564]) ).
fof(f3568,plain,
( divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f3565,f131]) ).
fof(f3570,plain,
( divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f3568]) ).
fof(f3571,plain,
divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f3570]) ).
fof(f4061,plain,
divide(divide(c,a),zero) = zero,
inference(resolution,[status(thm)],[f1935,f49]) ).
fof(f4069,plain,
divide(c,a) = zero,
inference(resolution,[status(thm)],[f4061,f53]) ).
fof(f4514,plain,
! [X0,X1,X2,X3] :
( divide(divide(divide(divide(X1,X2),X3),X0),divide(X1,X0)) = divide(divide(divide(divide(X1,X2),X3),X1),X0)
| divide(divide(zero,X0),divide(divide(divide(divide(X1,X2),X3),X0),divide(X1,X0))) != zero ),
inference(paramodulation,[status(thm)],[f3417,f127]) ).
fof(f4605,plain,
! [X0,X1,X2,X3] :
( divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3)) = divide(divide(divide(divide(X0,X1),X2),X0),X3)
| divide(zero,divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3))) != zero ),
inference(forward_demodulation,[status(thm)],[f29,f4514]) ).
fof(f4606,plain,
! [X0,X1,X2,X3] :
( divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3)) = divide(divide(divide(divide(X0,X1),X2),X0),X3)
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f4605]) ).
fof(f4607,plain,
! [X0,X1,X2,X3] :
( divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3)) = divide(zero,X3)
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f3417,f4606]) ).
fof(f4608,plain,
! [X0,X1,X2,X3] :
( divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3)) = zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f4607]) ).
fof(f4609,plain,
! [X0,X1,X2,X3] : divide(divide(divide(divide(X0,X1),X2),X3),divide(X0,X3)) = zero,
inference(trivial_equality_resolution,[status(thm)],[f4608]) ).
fof(f5372,plain,
! [X0,X1,X2,X3,X4] : divide(divide(divide(divide(divide(divide(X0,X1),X2),X3),X4),X0),zero) = zero,
inference(paramodulation,[status(thm)],[f3417,f4609]) ).
fof(f7052,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f3571,f131]) ).
fof(f7054,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f7052]) ).
fof(f7055,plain,
divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f7054]) ).
fof(f7058,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f7055,f131]) ).
fof(f7060,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f7058]) ).
fof(f7061,plain,
divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f7060]) ).
fof(f7064,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f7061,f131]) ).
fof(f7066,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f7064]) ).
fof(f7067,plain,
divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f7066]) ).
fof(f7070,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| divide(zero,divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero)) != zero ),
inference(resolution,[status(thm)],[f7067,f131]) ).
fof(f7072,plain,
( divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f29,f7070]) ).
fof(f7073,plain,
divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(divide(b,d),zero),zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero,
inference(trivial_equality_resolution,[status(thm)],[f7072]) ).
fof(f8093,plain,
divide(divide(b,zero),divide(divide(identity,c),a)) = zero,
inference(paramodulation,[status(thm)],[f4069,f315]) ).
fof(f8149,plain,
divide(divide(b,zero),divide(d,a)) = zero,
inference(forward_demodulation,[status(thm)],[f23,f8093]) ).
fof(f9162,plain,
( divide(divide(b,zero),divide(d,a)) = divide(divide(b,divide(d,a)),zero)
| ~ less_equal(zero,divide(divide(b,divide(d,a)),zero)) ),
inference(paramodulation,[status(thm)],[f8149,f287]) ).
fof(f9208,plain,
( zero = divide(divide(b,divide(d,a)),zero)
| ~ less_equal(zero,divide(divide(b,divide(d,a)),zero)) ),
inference(forward_demodulation,[status(thm)],[f8149,f9162]) ).
fof(f9209,plain,
zero = divide(divide(b,divide(d,a)),zero),
inference(forward_subsumption_resolution,[status(thm)],[f9208,f17]) ).
fof(f9273,plain,
divide(b,divide(d,a)) = zero,
inference(resolution,[status(thm)],[f9209,f53]) ).
fof(f9428,plain,
( divide(divide(b,divide(d,a)),d) = divide(divide(b,d),zero)
| ~ less_equal(divide(zero,d),divide(divide(b,d),zero)) ),
inference(paramodulation,[status(thm)],[f9273,f286]) ).
fof(f9468,plain,
( divide(divide(b,divide(d,a)),d) = divide(divide(b,d),zero)
| ~ less_equal(zero,divide(divide(b,d),zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f9428]) ).
fof(f9469,plain,
( divide(zero,d) = divide(divide(b,d),zero)
| ~ less_equal(zero,divide(divide(b,d),zero)) ),
inference(forward_demodulation,[status(thm)],[f9273,f9468]) ).
fof(f9470,plain,
( zero = divide(divide(b,d),zero)
| ~ less_equal(zero,divide(divide(b,d),zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f9469]) ).
fof(f9471,plain,
divide(divide(divide(divide(divide(divide(divide(divide(divide(zero,zero),zero),zero),zero),zero),zero),zero),zero),zero) != zero,
inference(backward_demodulation,[status(thm)],[f9482,f7073]) ).
fof(f9482,plain,
zero = divide(divide(b,d),zero),
inference(forward_subsumption_resolution,[status(thm)],[f9470,f17]) ).
fof(f9532,plain,
divide(divide(divide(zero,zero),zero),zero) != zero,
inference(forward_demodulation,[status(thm)],[f5372,f9471]) ).
fof(f9533,plain,
zero != zero,
inference(forward_demodulation,[status(thm)],[f3417,f9532]) ).
fof(f9534,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f9533]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HEN009-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:49:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.51 % Refutation found
% 0.09/0.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.39/0.54 % Elapsed time: 0.155021 seconds
% 0.39/0.54 % CPU time: 1.019385 seconds
% 0.39/0.54 % Total memory used: 92.263 MB
% 0.39/0.54 % Net memory used: 91.487 MB
%------------------------------------------------------------------------------