%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:24 PM UTC 2026
% Result : Unsatisfiable 26.09s 3.72s
% Output : CNFRefutation 26.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 12
% Syntax : Number of formulae : 213 ( 129 unt; 0 def)
% Number of atoms : 301 ( 211 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 180 ( 92 ~; 88 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 254 ( 254 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : less_equal(divide(X,Y),X),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : less_equal(zero,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : less_equal(X,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
divide(identity,a) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
divide(identity,b) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
divide(identity,c) = e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
divide(identity,d) = g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
divide(c,g) != divide(d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,plain,
! [X0,X1] :
( divide(X0,X1) = zero
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f15,plain,
! [X0,X1] :
( less_equal(X0,X1)
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f16,plain,
! [X0,X1] : less_equal(divide(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f17,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(f18,plain,
! [X0] : less_equal(zero,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f19,plain,
! [X0,X1] :
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f20,plain,
! [X0] : less_equal(X0,identity),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f22,plain,
divide(identity,a) = c,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f23,plain,
divide(identity,b) = d,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f24,plain,
divide(identity,c) = e,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f25,plain,
divide(identity,d) = g,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f26,plain,
divide(c,g) != divide(d,e),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f36,plain,
! [X0,X1] : divide(divide(X0,X1),X0) = zero,
inference(resolution,[status(thm)],[f14,f16]) ).
fof(f37,plain,
! [X0] : divide(zero,X0) = zero,
inference(resolution,[status(thm)],[f14,f18]) ).
fof(f38,plain,
! [X0] : divide(X0,identity) = zero,
inference(resolution,[status(thm)],[f14,f20]) ).
fof(f55,plain,
! [X0,X1] :
( X0 = divide(X0,X1)
| ~ less_equal(X0,divide(X0,X1)) ),
inference(resolution,[status(thm)],[f19,f16]) ).
fof(f56,plain,
! [X0] :
( X0 = zero
| ~ less_equal(X0,zero) ),
inference(resolution,[status(thm)],[f19,f18]) ).
fof(f58,plain,
! [X0,X1] :
( divide(X1,X0) != zero
| X0 = X1
| ~ less_equal(X0,X1) ),
inference(resolution,[status(thm)],[f19,f15]) ).
fof(f59,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)],[f17,f19]) ).
fof(f60,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = zero,
inference(resolution,[status(thm)],[f17,f14]) ).
fof(f64,plain,
! [X0] : less_equal(divide(g,divide(X0,d)),divide(divide(identity,X0),d)),
inference(paramodulation,[status(thm)],[f25,f17]) ).
fof(f65,plain,
! [X0] : less_equal(divide(e,divide(X0,c)),divide(divide(identity,X0),c)),
inference(paramodulation,[status(thm)],[f24,f17]) ).
fof(f66,plain,
! [X0] : less_equal(divide(d,divide(X0,b)),divide(divide(identity,X0),b)),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f67,plain,
! [X0] : less_equal(divide(c,divide(X0,a)),divide(divide(identity,X0),a)),
inference(paramodulation,[status(thm)],[f22,f17]) ).
fof(f69,plain,
! [X0,X1,X2] : less_equal(divide(divide(X0,X1),zero),divide(divide(X0,divide(X1,X2)),X1)),
inference(paramodulation,[status(thm)],[f36,f17]) ).
fof(f70,plain,
! [X0,X1] : less_equal(divide(divide(X0,X1),zero),divide(divide(X0,zero),X1)),
inference(paramodulation,[status(thm)],[f37,f17]) ).
fof(f71,plain,
! [X0] : less_equal(divide(divide(X0,d),g),divide(divide(X0,identity),d)),
inference(paramodulation,[status(thm)],[f25,f17]) ).
fof(f72,plain,
! [X0] : less_equal(divide(divide(X0,c),e),divide(divide(X0,identity),c)),
inference(paramodulation,[status(thm)],[f24,f17]) ).
fof(f73,plain,
! [X0] : less_equal(divide(divide(X0,b),d),divide(divide(X0,identity),b)),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f74,plain,
! [X0] : less_equal(divide(divide(X0,a),c),divide(divide(X0,identity),a)),
inference(paramodulation,[status(thm)],[f22,f17]) ).
fof(f93,plain,
! [X0] : less_equal(divide(divide(X0,d),g),divide(zero,d)),
inference(forward_demodulation,[status(thm)],[f38,f71]) ).
fof(f94,plain,
! [X0] : less_equal(divide(divide(X0,d),g),zero),
inference(forward_demodulation,[status(thm)],[f37,f93]) ).
fof(f95,plain,
! [X0] : less_equal(divide(divide(X0,c),e),divide(zero,c)),
inference(forward_demodulation,[status(thm)],[f38,f72]) ).
fof(f96,plain,
! [X0] : less_equal(divide(divide(X0,c),e),zero),
inference(forward_demodulation,[status(thm)],[f37,f95]) ).
fof(f97,plain,
! [X0] : less_equal(divide(divide(X0,b),d),divide(zero,b)),
inference(forward_demodulation,[status(thm)],[f38,f73]) ).
fof(f98,plain,
! [X0] : less_equal(divide(divide(X0,b),d),zero),
inference(forward_demodulation,[status(thm)],[f37,f97]) ).
fof(f99,plain,
! [X0] : less_equal(divide(divide(X0,a),c),divide(zero,a)),
inference(forward_demodulation,[status(thm)],[f38,f74]) ).
fof(f100,plain,
! [X0] : less_equal(divide(divide(X0,a),c),zero),
inference(forward_demodulation,[status(thm)],[f37,f99]) ).
fof(f113,plain,
! [X0] :
( divide(X0,zero) != zero
| X0 = zero ),
inference(resolution,[status(thm)],[f56,f15]) ).
fof(f127,plain,
! [X0,X1] :
( divide(X0,divide(X0,X1)) != zero
| X0 = divide(X0,X1) ),
inference(resolution,[status(thm)],[f55,f15]) ).
fof(f141,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,X2),X1),divide(divide(X0,X1),divide(X2,X1))) != zero
| divide(divide(X0,X1),divide(X2,X1)) = divide(divide(X0,X2),X1) ),
inference(resolution,[status(thm)],[f58,f17]) ).
fof(f145,plain,
! [X0,X1] :
( divide(X0,X1) != zero
| divide(X1,X0) != zero
| X0 = X1 ),
inference(resolution,[status(thm)],[f58,f15]) ).
fof(f146,plain,
! [X0] : divide(divide(X0,d),g) = zero,
inference(resolution,[status(thm)],[f94,f56]) ).
fof(f167,plain,
! [X0,X1] :
( divide(divide(X0,X1),X0) = divide(divide(X0,X0),divide(X1,X0))
| ~ less_equal(zero,divide(divide(X0,X0),divide(X1,X0))) ),
inference(paramodulation,[status(thm)],[f36,f59]) ).
fof(f169,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)],[f36,f59]) ).
fof(f174,plain,
! [X0] :
( divide(divide(identity,a),X0) = divide(divide(identity,X0),divide(a,X0))
| ~ less_equal(divide(c,X0),divide(divide(identity,X0),divide(a,X0))) ),
inference(paramodulation,[status(thm)],[f22,f59]) ).
fof(f191,plain,
! [X0,X1] :
( zero = divide(divide(X0,X0),divide(X1,X0))
| ~ less_equal(zero,divide(divide(X0,X0),divide(X1,X0))) ),
inference(forward_demodulation,[status(thm)],[f36,f167]) ).
fof(f193,plain,
! [X0,X1] : zero = divide(divide(X0,X0),divide(X1,X0)),
inference(forward_subsumption_resolution,[status(thm)],[f191,f18]) ).
fof(f198,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)],[f37,f169]) ).
fof(f199,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)],[f36,f198]) ).
fof(f200,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)],[f37,f199]) ).
fof(f202,plain,
! [X0,X1,X2] : zero = divide(divide(divide(X0,X1),X2),divide(X0,X2)),
inference(forward_subsumption_resolution,[status(thm)],[f200,f18]) ).
fof(f212,plain,
! [X0] :
( divide(c,X0) = divide(divide(identity,X0),divide(a,X0))
| ~ less_equal(divide(c,X0),divide(divide(identity,X0),divide(a,X0))) ),
inference(forward_demodulation,[status(thm)],[f22,f174]) ).
fof(f289,plain,
! [X0] :
( divide(divide(X0,d),g) = divide(divide(X0,g),divide(d,g))
| ~ less_equal(zero,divide(divide(X0,g),divide(d,g))) ),
inference(paramodulation,[status(thm)],[f146,f59]) ).
fof(f301,plain,
! [X0] :
( zero = divide(divide(X0,g),divide(d,g))
| ~ less_equal(zero,divide(divide(X0,g),divide(d,g))) ),
inference(forward_demodulation,[status(thm)],[f146,f289]) ).
fof(f302,plain,
! [X0] : zero = divide(divide(X0,g),divide(d,g)),
inference(forward_subsumption_resolution,[status(thm)],[f301,f18]) ).
fof(f323,plain,
! [X0] : zero = divide(divide(X0,X0),zero),
inference(paramodulation,[status(thm)],[f36,f193]) ).
fof(f364,plain,
! [X0] : divide(X0,X0) = zero,
inference(resolution,[status(thm)],[f323,f113]) ).
fof(f469,plain,
! [X0] : divide(divide(X0,c),e) = zero,
inference(resolution,[status(thm)],[f96,f56]) ).
fof(f494,plain,
! [X0] : divide(divide(c,divide(X0,a)),divide(divide(identity,X0),a)) = zero,
inference(paramodulation,[status(thm)],[f22,f60]) ).
fof(f518,plain,
! [X0] : divide(divide(divide(identity,X0),divide(b,X0)),divide(d,X0)) = zero,
inference(paramodulation,[status(thm)],[f23,f60]) ).
fof(f526,plain,
! [X0,X1,X2,X3] :
( 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))
| ~ less_equal(divide(zero,X0),divide(divide(divide(divide(X1,X2),divide(X3,X2)),X0),divide(divide(divide(X1,X3),X2),X0))) ),
inference(paramodulation,[status(thm)],[f60,f59]) ).
fof(f564,plain,
! [X0,X1,X2,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))
| ~ less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))) ),
inference(forward_demodulation,[status(thm)],[f37,f526]) ).
fof(f565,plain,
! [X0,X1,X2,X3] :
( divide(zero,X3) = divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))
| ~ less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))) ),
inference(forward_demodulation,[status(thm)],[f60,f564]) ).
fof(f566,plain,
! [X0,X1,X2,X3] :
( zero = divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))
| ~ less_equal(zero,divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3))) ),
inference(forward_demodulation,[status(thm)],[f37,f565]) ).
fof(f568,plain,
! [X0,X1,X2,X3] : zero = divide(divide(divide(divide(X0,X1),divide(X2,X1)),X3),divide(divide(divide(X0,X2),X1),X3)),
inference(forward_subsumption_resolution,[status(thm)],[f566,f18]) ).
fof(f579,plain,
! [X0] :
( divide(divide(X0,c),e) = divide(divide(X0,e),divide(c,e))
| ~ less_equal(zero,divide(divide(X0,e),divide(c,e))) ),
inference(paramodulation,[status(thm)],[f469,f59]) ).
fof(f594,plain,
! [X0] :
( zero = divide(divide(X0,e),divide(c,e))
| ~ less_equal(zero,divide(divide(X0,e),divide(c,e))) ),
inference(forward_demodulation,[status(thm)],[f469,f579]) ).
fof(f596,plain,
! [X0] : zero = divide(divide(X0,e),divide(c,e)),
inference(forward_subsumption_resolution,[status(thm)],[f594,f18]) ).
fof(f613,plain,
! [X0] : divide(divide(X0,b),d) = zero,
inference(resolution,[status(thm)],[f98,f56]) ).
fof(f670,plain,
! [X0] : divide(divide(X0,a),c) = zero,
inference(resolution,[status(thm)],[f100,f56]) ).
fof(f808,plain,
less_equal(divide(g,divide(b,d)),zero),
inference(paramodulation,[status(thm)],[f613,f64]) ).
fof(f902,plain,
divide(g,divide(b,d)) = zero,
inference(resolution,[status(thm)],[f808,f56]) ).
fof(f909,plain,
( divide(divide(b,d),g) != zero
| divide(b,d) = g ),
inference(resolution,[status(thm)],[f902,f145]) ).
fof(f926,plain,
( zero != zero
| divide(b,d) = g ),
inference(forward_demodulation,[status(thm)],[f146,f909]) ).
fof(f929,plain,
divide(b,d) = g,
inference(trivial_equality_resolution,[status(thm)],[f926]) ).
fof(f978,plain,
divide(g,b) = zero,
inference(paramodulation,[status(thm)],[f929,f36]) ).
fof(f1002,plain,
less_equal(divide(e,divide(a,c)),zero),
inference(paramodulation,[status(thm)],[f670,f65]) ).
fof(f1062,plain,
divide(e,divide(a,c)) = zero,
inference(resolution,[status(thm)],[f1002,f56]) ).
fof(f1069,plain,
! [X0] :
( divide(divide(divide(identity,X0),b),divide(d,divide(X0,b))) != zero
| divide(d,divide(X0,b)) = divide(divide(identity,X0),b) ),
inference(resolution,[status(thm)],[f66,f58]) ).
fof(f1077,plain,
less_equal(divide(d,divide(d,b)),divide(g,b)),
inference(paramodulation,[status(thm)],[f25,f66]) ).
fof(f1087,plain,
less_equal(divide(d,divide(d,b)),zero),
inference(forward_demodulation,[status(thm)],[f978,f1077]) ).
fof(f1095,plain,
( divide(divide(a,c),e) != zero
| divide(a,c) = e ),
inference(resolution,[status(thm)],[f1062,f145]) ).
fof(f1112,plain,
( zero != zero
| divide(a,c) = e ),
inference(forward_demodulation,[status(thm)],[f469,f1095]) ).
fof(f1115,plain,
divide(a,c) = e,
inference(trivial_equality_resolution,[status(thm)],[f1112]) ).
fof(f1164,plain,
divide(e,a) = zero,
inference(paramodulation,[status(thm)],[f1115,f36]) ).
fof(f1227,plain,
less_equal(divide(c,divide(c,a)),divide(e,a)),
inference(paramodulation,[status(thm)],[f24,f67]) ).
fof(f1236,plain,
less_equal(divide(c,divide(c,a)),zero),
inference(forward_demodulation,[status(thm)],[f1164,f1227]) ).
fof(f1304,plain,
divide(d,divide(d,b)) = zero,
inference(resolution,[status(thm)],[f1087,f56]) ).
fof(f1311,plain,
d = divide(d,b),
inference(resolution,[status(thm)],[f1304,f127]) ).
fof(f1499,plain,
divide(c,divide(c,a)) = zero,
inference(resolution,[status(thm)],[f1236,f56]) ).
fof(f1506,plain,
c = divide(c,a),
inference(resolution,[status(thm)],[f1499,f127]) ).
fof(f1687,plain,
! [X0,X1,X2] : zero = divide(divide(divide(divide(X0,X1),X2),X0),zero),
inference(paramodulation,[status(thm)],[f36,f202]) ).
fof(f2250,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),X2),X0) = zero,
inference(resolution,[status(thm)],[f1687,f113]) ).
fof(f2811,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,divide(X1,X2)),X1),divide(divide(X0,X1),zero)) != zero
| divide(divide(X0,X1),zero) = divide(divide(X0,divide(X1,X2)),X1) ),
inference(resolution,[status(thm)],[f69,f58]) ).
fof(f2857,plain,
! [X0] : less_equal(divide(divide(divide(X0,e),c),zero),divide(zero,c)),
inference(paramodulation,[status(thm)],[f596,f69]) ).
fof(f2858,plain,
! [X0] : less_equal(divide(divide(divide(X0,g),d),zero),divide(zero,d)),
inference(paramodulation,[status(thm)],[f302,f69]) ).
fof(f2951,plain,
! [X0] : less_equal(divide(divide(divide(X0,e),c),zero),zero),
inference(forward_demodulation,[status(thm)],[f37,f2857]) ).
fof(f2952,plain,
! [X0] : less_equal(divide(divide(divide(X0,g),d),zero),zero),
inference(forward_demodulation,[status(thm)],[f37,f2858]) ).
fof(f3254,plain,
! [X0] : less_equal(divide(divide(X0,divide(X0,zero)),zero),zero),
inference(paramodulation,[status(thm)],[f364,f70]) ).
fof(f3481,plain,
! [X0] : divide(divide(X0,divide(X0,zero)),zero) = zero,
inference(resolution,[status(thm)],[f3254,f56]) ).
fof(f3501,plain,
! [X0] : divide(X0,divide(X0,zero)) = zero,
inference(resolution,[status(thm)],[f3481,f113]) ).
fof(f3594,plain,
! [X0] : X0 = divide(X0,zero),
inference(resolution,[status(thm)],[f3501,f127]) ).
fof(f3651,plain,
! [X0,X1] :
( divide(divide(X0,X1),divide(X1,zero)) = divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),divide(X1,zero)),divide(divide(X0,divide(X1,zero)),zero)) ),
inference(paramodulation,[status(thm)],[f3501,f59]) ).
fof(f3704,plain,
! [X0] : less_equal(divide(divide(X0,e),c),zero),
inference(backward_demodulation,[status(thm)],[f3594,f2951]) ).
fof(f3705,plain,
! [X0] : less_equal(divide(divide(X0,g),d),zero),
inference(backward_demodulation,[status(thm)],[f3594,f2952]) ).
fof(f3759,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,divide(X1,X2)),X1),divide(X0,X1)) != zero
| divide(divide(X0,X1),zero) = divide(divide(X0,divide(X1,X2)),X1) ),
inference(backward_demodulation,[status(thm)],[f3594,f2811]) ).
fof(f3898,plain,
! [X0,X1] :
( divide(divide(X0,X1),divide(X1,zero)) = divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),X1),divide(divide(X0,divide(X1,zero)),zero)) ),
inference(forward_demodulation,[status(thm)],[f3594,f3651]) ).
fof(f3899,plain,
! [X0,X1] :
( divide(divide(X0,X1),divide(X1,zero)) = divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,divide(X1,zero))) ),
inference(forward_demodulation,[status(thm)],[f3594,f3898]) ).
fof(f3900,plain,
! [X0,X1] :
( divide(divide(X0,X1),divide(X1,zero)) = divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f3594,f3899]) ).
fof(f3901,plain,
! [X0,X1] :
( divide(divide(X0,X1),X1) = divide(divide(X0,divide(X1,zero)),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f3594,f3900]) ).
fof(f3902,plain,
! [X0,X1] :
( divide(divide(X0,X1),X1) = divide(divide(X0,X1),divide(X1,divide(X1,zero)))
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f3594,f3901]) ).
fof(f3903,plain,
! [X0,X1] :
( divide(divide(X0,X1),X1) = divide(divide(X0,X1),zero)
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f3501,f3902]) ).
fof(f3904,plain,
! [X0,X1] :
( divide(divide(X0,X1),X1) = divide(X0,X1)
| ~ less_equal(divide(divide(X0,X1),X1),divide(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f3594,f3903]) ).
fof(f3906,plain,
! [X0,X1] : divide(divide(X0,X1),X1) = divide(X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f16]) ).
fof(f3975,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,divide(X1,X2)),X1),divide(X0,X1)) != zero
| divide(X0,X1) = divide(divide(X0,divide(X1,X2)),X1) ),
inference(forward_demodulation,[status(thm)],[f3594,f3759]) ).
fof(f3976,plain,
! [X0,X1,X2] :
( zero != zero
| divide(X0,X1) = divide(divide(X0,divide(X1,X2)),X1) ),
inference(forward_demodulation,[status(thm)],[f202,f3975]) ).
fof(f3984,plain,
! [X0,X1,X2] : divide(X0,X1) = divide(divide(X0,divide(X1,X2)),X1),
inference(trivial_equality_resolution,[status(thm)],[f3976]) ).
fof(f4219,plain,
! [X0] :
( divide(divide(divide(c,X0),a),divide(c,divide(X0,a))) != zero
| divide(divide(c,a),divide(X0,a)) = divide(divide(c,X0),a) ),
inference(paramodulation,[status(thm)],[f1506,f141]) ).
fof(f4220,plain,
! [X0] :
( divide(divide(divide(d,X0),b),divide(d,divide(X0,b))) != zero
| divide(divide(d,b),divide(X0,b)) = divide(divide(d,X0),b) ),
inference(paramodulation,[status(thm)],[f1311,f141]) ).
fof(f4389,plain,
! [X0] :
( divide(divide(divide(c,X0),a),divide(c,divide(X0,a))) != zero
| divide(c,divide(X0,a)) = divide(divide(c,X0),a) ),
inference(forward_demodulation,[status(thm)],[f1506,f4219]) ).
fof(f4390,plain,
! [X0] :
( divide(divide(divide(d,X0),b),divide(d,divide(X0,b))) != zero
| divide(d,divide(X0,b)) = divide(divide(d,X0),b) ),
inference(forward_demodulation,[status(thm)],[f1311,f4220]) ).
fof(f4720,plain,
! [X0,X1,X2] :
( divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1))) != zero
| divide(divide(divide(X0,X1),X1),divide(X2,X1)) = divide(divide(divide(X0,X1),X2),X1) ),
inference(paramodulation,[status(thm)],[f3906,f141]) ).
fof(f4789,plain,
! [X0,X1,X2] :
( divide(divide(divide(divide(X0,X1),X2),X1),divide(divide(X0,X1),divide(X2,X1))) != zero
| divide(divide(X0,X1),divide(X2,X1)) = divide(divide(divide(X0,X1),X2),X1) ),
inference(forward_demodulation,[status(thm)],[f3906,f4720]) ).
fof(f4794,plain,
! [X0] : divide(divide(X0,e),c) = zero,
inference(resolution,[status(thm)],[f3704,f56]) ).
fof(f4914,plain,
! [X0] : divide(divide(X0,g),d) = zero,
inference(resolution,[status(thm)],[f3705,f56]) ).
fof(f6241,plain,
! [X0,X1,X2,X3] : divide(divide(divide(X0,X1),X2),divide(X0,divide(X1,X3))) = zero,
inference(paramodulation,[status(thm)],[f3984,f2250]) ).
fof(f6257,plain,
! [X0,X1,X2] : divide(divide(X0,X1),divide(X0,divide(X1,X2))) = zero,
inference(paramodulation,[status(thm)],[f3984,f36]) ).
fof(f6258,plain,
! [X0,X1,X2] : less_equal(divide(X0,X1),divide(X0,divide(X1,X2))),
inference(paramodulation,[status(thm)],[f3984,f16]) ).
fof(f6304,plain,
! [X0] :
( zero != zero
| divide(d,divide(X0,b)) = divide(divide(d,X0),b) ),
inference(backward_demodulation,[status(thm)],[f6241,f4390]) ).
fof(f6305,plain,
! [X0] :
( zero != zero
| divide(c,divide(X0,a)) = divide(divide(c,X0),a) ),
inference(backward_demodulation,[status(thm)],[f6241,f4389]) ).
fof(f6308,plain,
! [X0,X1,X2] :
( zero != zero
| divide(divide(X0,X1),divide(X2,X1)) = divide(divide(divide(X0,X1),X2),X1) ),
inference(backward_demodulation,[status(thm)],[f6241,f4789]) ).
fof(f6317,plain,
! [X0] : divide(d,divide(X0,b)) = divide(divide(d,X0),b),
inference(trivial_equality_resolution,[status(thm)],[f6304]) ).
fof(f6321,plain,
! [X0] : divide(c,divide(X0,a)) = divide(divide(c,X0),a),
inference(trivial_equality_resolution,[status(thm)],[f6305]) ).
fof(f6333,plain,
! [X0,X1,X2] : divide(divide(X0,X1),divide(X2,X1)) = divide(divide(divide(X0,X1),X2),X1),
inference(trivial_equality_resolution,[status(thm)],[f6308]) ).
fof(f6400,plain,
! [X0] : less_equal(divide(X0,a),divide(X0,e)),
inference(paramodulation,[status(thm)],[f1115,f6258]) ).
fof(f6403,plain,
! [X0] : less_equal(divide(X0,b),divide(X0,g)),
inference(paramodulation,[status(thm)],[f929,f6258]) ).
fof(f6498,plain,
less_equal(c,divide(c,e)),
inference(paramodulation,[status(thm)],[f1506,f6400]) ).
fof(f6507,plain,
less_equal(c,divide(identity,e)),
inference(paramodulation,[status(thm)],[f22,f6400]) ).
fof(f6527,plain,
c = divide(c,e),
inference(resolution,[status(thm)],[f6498,f55]) ).
fof(f6555,plain,
! [X0] :
( divide(divide(divide(c,X0),e),divide(c,divide(X0,e))) != zero
| divide(divide(c,e),divide(X0,e)) = divide(divide(c,X0),e) ),
inference(paramodulation,[status(thm)],[f6527,f141]) ).
fof(f6584,plain,
! [X0] :
( divide(divide(divide(c,X0),e),divide(c,divide(X0,e))) != zero
| divide(c,divide(X0,e)) = divide(divide(c,X0),e) ),
inference(forward_demodulation,[status(thm)],[f6527,f6555]) ).
fof(f6585,plain,
! [X0] :
( zero != zero
| divide(c,divide(X0,e)) = divide(divide(c,X0),e) ),
inference(forward_demodulation,[status(thm)],[f6241,f6584]) ).
fof(f6586,plain,
! [X0] : divide(c,divide(X0,e)) = divide(divide(c,X0),e),
inference(trivial_equality_resolution,[status(thm)],[f6585]) ).
fof(f6689,plain,
( divide(divide(identity,e),c) != zero
| c = divide(identity,e) ),
inference(resolution,[status(thm)],[f6507,f58]) ).
fof(f6692,plain,
( zero != zero
| c = divide(identity,e) ),
inference(forward_demodulation,[status(thm)],[f4794,f6689]) ).
fof(f6696,plain,
c = divide(identity,e),
inference(trivial_equality_resolution,[status(thm)],[f6692]) ).
fof(f6784,plain,
less_equal(d,divide(d,g)),
inference(paramodulation,[status(thm)],[f1311,f6403]) ).
fof(f6795,plain,
less_equal(d,divide(identity,g)),
inference(paramodulation,[status(thm)],[f23,f6403]) ).
fof(f6819,plain,
d = divide(d,g),
inference(resolution,[status(thm)],[f6784,f55]) ).
fof(f6848,plain,
! [X0] :
( divide(divide(divide(d,X0),g),divide(d,divide(X0,g))) != zero
| divide(divide(d,g),divide(X0,g)) = divide(divide(d,X0),g) ),
inference(paramodulation,[status(thm)],[f6819,f141]) ).
fof(f6878,plain,
! [X0] :
( divide(divide(divide(d,X0),g),divide(d,divide(X0,g))) != zero
| divide(d,divide(X0,g)) = divide(divide(d,X0),g) ),
inference(forward_demodulation,[status(thm)],[f6819,f6848]) ).
fof(f6879,plain,
! [X0] :
( zero != zero
| divide(d,divide(X0,g)) = divide(divide(d,X0),g) ),
inference(forward_demodulation,[status(thm)],[f6241,f6878]) ).
fof(f6880,plain,
! [X0] : divide(d,divide(X0,g)) = divide(divide(d,X0),g),
inference(trivial_equality_resolution,[status(thm)],[f6879]) ).
fof(f6991,plain,
( divide(divide(identity,g),d) != zero
| d = divide(identity,g) ),
inference(resolution,[status(thm)],[f6795,f58]) ).
fof(f6994,plain,
( zero != zero
| d = divide(identity,g) ),
inference(forward_demodulation,[status(thm)],[f4914,f6991]) ).
fof(f6999,plain,
d = divide(identity,g),
inference(trivial_equality_resolution,[status(thm)],[f6994]) ).
fof(f7002,plain,
( divide(c,g) = divide(divide(identity,g),divide(a,g))
| ~ less_equal(divide(c,g),divide(d,divide(a,g))) ),
inference(paramodulation,[status(thm)],[f6999,f212]) ).
fof(f7010,plain,
less_equal(divide(c,divide(g,a)),divide(d,a)),
inference(paramodulation,[status(thm)],[f6999,f67]) ).
fof(f7043,plain,
( divide(c,g) = divide(d,divide(a,g))
| ~ less_equal(divide(c,g),divide(d,divide(a,g))) ),
inference(forward_demodulation,[status(thm)],[f6999,f7002]) ).
fof(f13020,plain,
divide(divide(c,divide(b,a)),divide(d,a)) = zero,
inference(paramodulation,[status(thm)],[f23,f494]) ).
fof(f16507,plain,
divide(divide(c,divide(b,e)),divide(d,e)) = zero,
inference(paramodulation,[status(thm)],[f6696,f518]) ).
fof(f21455,plain,
! [X0,X1,X2] : zero = divide(divide(divide(X0,X1),X2),divide(divide(divide(X0,X2),X1),X2)),
inference(paramodulation,[status(thm)],[f3984,f568]) ).
fof(f22009,plain,
! [X0,X1,X2] :
( zero != zero
| divide(divide(X0,X1),divide(X2,X1)) = divide(divide(X0,X2),X1) ),
inference(backward_demodulation,[status(thm)],[f22010,f141]) ).
fof(f22010,plain,
! [X0,X1,X2] : zero = divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),divide(X1,X2))),
inference(forward_demodulation,[status(thm)],[f6333,f21455]) ).
fof(f23120,plain,
! [X0,X1,X2] : divide(divide(X0,X1),divide(X2,X1)) = divide(divide(X0,X2),X1),
inference(trivial_equality_resolution,[status(thm)],[f22009]) ).
fof(f29479,plain,
( divide(divide(c,b),divide(d,divide(e,b))) != zero
| divide(d,divide(e,b)) = divide(divide(identity,e),b) ),
inference(paramodulation,[status(thm)],[f6696,f1069]) ).
fof(f29483,plain,
( divide(divide(c,b),divide(d,divide(a,b))) != zero
| divide(d,divide(a,b)) = divide(divide(identity,a),b) ),
inference(paramodulation,[status(thm)],[f22,f1069]) ).
fof(f29539,plain,
( divide(divide(c,b),divide(d,divide(e,b))) != zero
| divide(d,divide(e,b)) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f6696,f29479]) ).
fof(f29545,plain,
( divide(divide(c,b),divide(d,divide(a,b))) != zero
| divide(d,divide(a,b)) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f22,f29483]) ).
fof(f38171,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1)) = zero,
inference(paramodulation,[status(thm)],[f23120,f6257]) ).
fof(f38172,plain,
! [X0,X1,X2] : less_equal(divide(divide(X0,X1),X2),divide(divide(X0,X2),X1)),
inference(paramodulation,[status(thm)],[f23120,f6258]) ).
fof(f40092,plain,
! [X0,X1,X2] :
( divide(divide(divide(X0,X2),X1),divide(divide(X0,X1),X2)) != zero
| divide(divide(X0,X1),X2) = divide(divide(X0,X2),X1) ),
inference(resolution,[status(thm)],[f38172,f58]) ).
fof(f40509,plain,
! [X0,X1,X2] :
( zero != zero
| divide(divide(X0,X1),X2) = divide(divide(X0,X2),X1) ),
inference(forward_demodulation,[status(thm)],[f38171,f40092]) ).
fof(f40658,plain,
! [X0,X1,X2] : divide(divide(X0,X1),X2) = divide(divide(X0,X2),X1),
inference(trivial_equality_resolution,[status(thm)],[f40509]) ).
fof(f41527,plain,
! [X0] : divide(c,X0) = divide(divide(c,X0),e),
inference(paramodulation,[status(thm)],[f6527,f40658]) ).
fof(f41528,plain,
! [X0] : divide(c,X0) = divide(divide(c,X0),a),
inference(paramodulation,[status(thm)],[f1506,f40658]) ).
fof(f41540,plain,
! [X0] : divide(d,X0) = divide(divide(d,X0),g),
inference(paramodulation,[status(thm)],[f6819,f40658]) ).
fof(f41541,plain,
! [X0] : divide(d,X0) = divide(divide(d,X0),b),
inference(paramodulation,[status(thm)],[f1311,f40658]) ).
fof(f42323,plain,
divide(divide(c,b),divide(d,e)) = zero,
inference(backward_demodulation,[status(thm)],[f42335,f16507]) ).
fof(f42335,plain,
! [X0] : divide(c,X0) = divide(c,divide(X0,e)),
inference(forward_demodulation,[status(thm)],[f6586,f41527]) ).
fof(f42342,plain,
less_equal(divide(c,g),divide(d,a)),
inference(backward_demodulation,[status(thm)],[f42354,f7010]) ).
fof(f42344,plain,
divide(divide(c,b),divide(d,a)) = zero,
inference(backward_demodulation,[status(thm)],[f42354,f13020]) ).
fof(f42354,plain,
! [X0] : divide(c,X0) = divide(c,divide(X0,a)),
inference(forward_demodulation,[status(thm)],[f6321,f41528]) ).
fof(f42394,plain,
( divide(c,g) = divide(d,a)
| ~ less_equal(divide(c,g),divide(d,divide(a,g))) ),
inference(backward_demodulation,[status(thm)],[f42404,f7043]) ).
fof(f42404,plain,
! [X0] : divide(d,X0) = divide(d,divide(X0,g)),
inference(forward_demodulation,[status(thm)],[f6880,f41540]) ).
fof(f42408,plain,
( divide(divide(c,b),divide(d,e)) != zero
| divide(d,divide(e,b)) = divide(c,b) ),
inference(backward_demodulation,[status(thm)],[f42423,f29539]) ).
fof(f42412,plain,
( divide(divide(c,b),divide(d,a)) != zero
| divide(d,divide(a,b)) = divide(c,b) ),
inference(backward_demodulation,[status(thm)],[f42423,f29545]) ).
fof(f42423,plain,
! [X0] : divide(d,X0) = divide(d,divide(X0,b)),
inference(forward_demodulation,[status(thm)],[f6317,f41541]) ).
fof(f43032,plain,
( divide(c,g) = divide(d,a)
| ~ less_equal(divide(c,g),divide(d,a)) ),
inference(forward_demodulation,[status(thm)],[f42404,f42394]) ).
fof(f43043,plain,
divide(c,g) = divide(d,a),
inference(forward_subsumption_resolution,[status(thm)],[f43032,f42342]) ).
fof(f43048,plain,
( divide(divide(c,b),divide(d,e)) != zero
| divide(d,e) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f42423,f42408]) ).
fof(f43049,plain,
( zero != zero
| divide(d,e) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f42323,f43048]) ).
fof(f43051,plain,
divide(c,g) != divide(c,b),
inference(backward_demodulation,[status(thm)],[f43058,f26]) ).
fof(f43058,plain,
divide(d,e) = divide(c,b),
inference(trivial_equality_resolution,[status(thm)],[f43049]) ).
fof(f43065,plain,
( divide(divide(c,b),divide(d,a)) != zero
| divide(d,a) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f42423,f42412]) ).
fof(f43066,plain,
( divide(divide(c,b),divide(d,a)) != zero
| divide(c,g) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f43043,f43065]) ).
fof(f43067,plain,
( zero != zero
| divide(c,g) = divide(c,b) ),
inference(forward_demodulation,[status(thm)],[f42344,f43066]) ).
fof(f43072,plain,
divide(c,g) = divide(c,b),
inference(trivial_equality_resolution,[status(thm)],[f43067]) ).
fof(f43288,plain,
divide(c,g) != divide(c,g),
inference(forward_demodulation,[status(thm)],[f43072,f43051]) ).
fof(f43289,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f43288]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:49:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 26.09/3.72 % Refutation found
% 26.09/3.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 26.09/3.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.69/3.83 % Elapsed time: 3.459323 seconds
% 4.69/3.83 % CPU time: 26.892845 seconds
% 4.69/3.83 % Total memory used: 400.407 MB
% 4.69/3.83 % Net memory used: 388.634 MB
%------------------------------------------------------------------------------