%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HEN009-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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 : Fri Sep 25 01:37:09 PM UTC 2026
% Result : Unsatisfiable 6.16s 1.33s
% Output : Proof 6.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 13
% Syntax : Number of formulae : 280 ( 268 unt; 0 def)
% Number of atoms : 296 ( 263 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 42 ( 26 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-4 aty)
% Number of variables : 264 ( 101 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,hypothesis,
divide(identity,a) != divide(identity,divide(identity,divide(identity,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_of_theorem) ).
fof(f7_nnf,plain,
divide(identity,a) != divide(identity,divide(identity,divide(identity,a))),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
divide(identity,a) != divide(identity,divide(identity,divide(identity,a))),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
divide(identity,a) != divide(identity,divide(identity,divide(identity,a))),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t14,plain,
ifeq(divide(identity,a),divide(identity,divide(identity,divide(identity,a))),false,true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f8,hypothesis,
divide(identity,a) = b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id_divide_a_is_b) ).
fof(f8_nnf,plain,
divide(identity,a) = b,
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
divide(identity,a) = b,
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t1,plain,
divide(identity,a) = b,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t41,plain,
divide(identity,a) = b,
inference(orient,[status(thm)],[t1]) ).
cnf(t1891,plain,
ifeq(b,divide(identity,divide(identity,divide(identity,a))),false,true) = true,
inference(step,[status(thm)],[t14,t41]) ).
cnf(t1892,plain,
ifeq(b,divide(identity,divide(identity,b)),false,true) = true,
inference(step,[status(thm)],[t1891,t41]) ).
cnf(f9,hypothesis,
divide(identity,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id_divide_b_is_c) ).
fof(f9_nnf,plain,
divide(identity,b) = c,
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
divide(identity,b) = c,
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t2,plain,
divide(identity,b) = c,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t37,plain,
divide(identity,b) = c,
inference(orient,[status(thm)],[t2]) ).
cnf(t1893,plain,
ifeq(b,divide(identity,c),false,true) = true,
inference(step,[status(thm)],[t1892,t37]) ).
cnf(f10,hypothesis,
divide(identity,c) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id_divide_c_is_d) ).
fof(f10_nnf,plain,
divide(identity,c) = d,
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
divide(identity,c) = d,
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t3,plain,
divide(identity,c) = d,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t45,plain,
divide(identity,c) = d,
inference(orient,[status(thm)],[t3]) ).
cnf(t1894,plain,
ifeq(b,d,false,true) = true,
inference(step,[status(thm)],[t1893,t45]) ).
cnf(t93,plain,
ifeq(b,d,false,true) = true,
inference(orient,[status(thm)],[t1894]) ).
cnf(f5,axiom,
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_and_equal) ).
fof(f5_nnf,plain,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t15,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t18,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(f2,axiom,
less_equal(divide(X,Y),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_smaller_than_numerator) ).
fof(f2_nnf,plain,
! [X,Y] : less_equal(divide(X,Y),X),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : less_equal(divide(X,Y),X),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
less_equal(divide(X0,X1),X0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t10,plain,
less_equal(divide(X1,X2),X1) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t52,plain,
less_equal(divide(X1,X2),X1) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(f1,axiom,
( less_equal(X,Y)
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal2) ).
fof(f1_nnf,plain,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( less_equal(X0,X1)
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t11,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t89,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(f0,axiom,
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal1) ).
fof(f0_nnf,plain,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( divide(X0,X1) = zero
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(less_equal(X0,X1),true,divide(X0,X1),zero) = zero,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(f3,axiom,
less_equal(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
fof(f3_nnf,plain,
! [X,Z,Y] : less_equal(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Z,Y] : less_equal(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t13,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi3]) ).
cnf(t23,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t33,plain,
zero = divide(divide(divide(divide(X1,X2),divide(divide(X1,X3),X2)),divide(divide(X3,X2),divide(divide(X1,X3),X2))),zero),
inference(cp,[status(thm)],[t23,t23]) ).
cnf(f4,axiom,
less_equal(zero,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_is_smallest) ).
fof(f4_nnf,plain,
! [X] : less_equal(zero,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : less_equal(zero,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
less_equal(zero,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t6,plain,
less_equal(zero,X1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t86,plain,
less_equal(zero,X1) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t88,plain,
zero = ifeq(less_equal(X1,zero),true,ifeq(true,true,X1,zero),zero),
inference(cp,[status(thm)],[t18,t86]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t1937,plain,
zero = ifeq(less_equal(X1,zero),true,X1,zero),
inference(step,[status(thm)],[t88,t17]) ).
cnf(t236,plain,
ifeq(less_equal(X1,zero),true,X1,zero) = zero,
inference(orient,[status(thm)],[t1937]) ).
cnf(hi4,axiom,
less_equal(zero,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t4,plain,
divide(zero,X1) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi4]) ).
cnf(t35,plain,
divide(zero,X1) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t36,plain,
zero = divide(divide(divide(X1,X2),zero),divide(divide(X1,zero),X2)),
inference(cp,[status(thm)],[t23,t35]) ).
cnf(t694,plain,
divide(divide(divide(X1,X2),zero),divide(divide(X1,zero),X2)) = zero,
inference(orient,[status(thm)],[t36]) ).
cnf(hi2,axiom,
less_equal(divide(X0,X1),X0) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t7,plain,
divide(divide(X1,X2),X1) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi2]) ).
cnf(t20,plain,
divide(divide(X1,X2),X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t27,plain,
zero = divide(divide(divide(X1,X1),divide(X2,X1)),zero),
inference(cp,[status(thm)],[t23,t20]) ).
cnf(t243,plain,
divide(divide(divide(X1,X1),divide(X2,X1)),zero) = zero,
inference(orient,[status(thm)],[t27]) ).
cnf(t244,plain,
zero = divide(divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t243,t35]) ).
cnf(t285,plain,
divide(divide(divide(X1,X1),zero),zero) = zero,
inference(orient,[status(thm)],[t244]) ).
cnf(t287,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,X1),zero),zero),true),
inference(cp,[status(thm)],[t89,t285]) ).
cnf(t1938,plain,
true = less_equal(divide(divide(X1,X1),zero),zero),
inference(step,[status(thm)],[t287,t17]) ).
cnf(t293,plain,
less_equal(divide(divide(X1,X1),zero),zero) = true,
inference(orient,[status(thm)],[t1938]) ).
cnf(t294,plain,
zero = ifeq(true,true,divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t236,t293]) ).
cnf(t1939,plain,
zero = divide(divide(X1,X1),zero),
inference(step,[status(thm)],[t294,t17]) ).
cnf(t298,plain,
divide(divide(X1,X1),zero) = zero,
inference(orient,[status(thm)],[t1939]) ).
cnf(t300,plain,
true = ifeq(zero,zero,less_equal(divide(X1,X1),zero),true),
inference(cp,[status(thm)],[t89,t298]) ).
cnf(t1940,plain,
true = less_equal(divide(X1,X1),zero),
inference(step,[status(thm)],[t300,t17]) ).
cnf(t307,plain,
less_equal(divide(X1,X1),zero) = true,
inference(orient,[status(thm)],[t1940]) ).
cnf(t308,plain,
zero = ifeq(true,true,divide(X1,X1),zero),
inference(cp,[status(thm)],[t236,t307]) ).
cnf(t1941,plain,
zero = divide(X1,X1),
inference(step,[status(thm)],[t308,t17]) ).
cnf(t312,plain,
divide(X1,X1) = zero,
inference(orient,[status(thm)],[t1941]) ).
cnf(t705,plain,
zero = divide(divide(divide(X1,divide(X1,zero)),zero),zero),
inference(cp,[status(thm)],[t694,t312]) ).
cnf(t810,plain,
divide(divide(divide(X1,divide(X1,zero)),zero),zero) = zero,
inference(orient,[status(thm)],[t705]) ).
cnf(t812,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,divide(X1,zero)),zero),zero),true),
inference(cp,[status(thm)],[t89,t810]) ).
cnf(t2017,plain,
true = less_equal(divide(divide(X1,divide(X1,zero)),zero),zero),
inference(step,[status(thm)],[t812,t17]) ).
cnf(t1078,plain,
less_equal(divide(divide(X1,divide(X1,zero)),zero),zero) = true,
inference(orient,[status(thm)],[t2017]) ).
cnf(t1079,plain,
zero = ifeq(true,true,divide(divide(X1,divide(X1,zero)),zero),zero),
inference(cp,[status(thm)],[t236,t1078]) ).
cnf(t2018,plain,
zero = divide(divide(X1,divide(X1,zero)),zero),
inference(step,[status(thm)],[t1079,t17]) ).
cnf(t1083,plain,
divide(divide(X1,divide(X1,zero)),zero) = zero,
inference(orient,[status(thm)],[t2018]) ).
cnf(t1085,plain,
true = ifeq(zero,zero,less_equal(divide(X1,divide(X1,zero)),zero),true),
inference(cp,[status(thm)],[t89,t1083]) ).
cnf(t2019,plain,
true = less_equal(divide(X1,divide(X1,zero)),zero),
inference(step,[status(thm)],[t1085,t17]) ).
cnf(t1098,plain,
less_equal(divide(X1,divide(X1,zero)),zero) = true,
inference(orient,[status(thm)],[t2019]) ).
cnf(t1099,plain,
zero = ifeq(true,true,divide(X1,divide(X1,zero)),zero),
inference(cp,[status(thm)],[t236,t1098]) ).
cnf(t2020,plain,
zero = divide(X1,divide(X1,zero)),
inference(step,[status(thm)],[t1099,t17]) ).
cnf(t1103,plain,
divide(X1,divide(X1,zero)) = zero,
inference(orient,[status(thm)],[t2020]) ).
cnf(t1105,plain,
true = ifeq(zero,zero,less_equal(X1,divide(X1,zero)),true),
inference(cp,[status(thm)],[t89,t1103]) ).
cnf(t2021,plain,
true = less_equal(X1,divide(X1,zero)),
inference(step,[status(thm)],[t1105,t17]) ).
cnf(t1119,plain,
less_equal(X1,divide(X1,zero)) = true,
inference(orient,[status(thm)],[t2021]) ).
cnf(t1121,plain,
divide(X1,zero) = ifeq(true,true,ifeq(less_equal(divide(X1,zero),X1),true,X1,divide(X1,zero)),divide(X1,zero)),
inference(cp,[status(thm)],[t18,t1119]) ).
cnf(t2022,plain,
divide(X1,zero) = ifeq(less_equal(divide(X1,zero),X1),true,X1,divide(X1,zero)),
inference(step,[status(thm)],[t1121,t17]) ).
cnf(t2023,plain,
divide(X1,zero) = ifeq(true,true,X1,divide(X1,zero)),
inference(step,[status(thm)],[t2022,t52]) ).
cnf(t2024,plain,
divide(X1,zero) = X1,
inference(step,[status(thm)],[t2023,t17]) ).
cnf(t1123,plain,
divide(X1,zero) = X1,
inference(orient,[status(thm)],[t2024]) ).
cnf(t2072,plain,
zero = divide(divide(divide(X1,X2),divide(divide(X1,X3),X2)),divide(divide(X3,X2),divide(divide(X1,X3),X2))),
inference(step,[status(thm)],[t33,t1123]) ).
cnf(t1422,plain,
divide(divide(divide(X1,X2),divide(divide(X1,X3),X2)),divide(divide(X3,X2),divide(divide(X1,X3),X2))) = zero,
inference(orient,[status(thm)],[t2072]) ).
cnf(t26,plain,
zero = divide(divide(divide(X1,X2),zero),divide(divide(X1,divide(X2,X3)),X2)),
inference(cp,[status(thm)],[t23,t20]) ).
cnf(t255,plain,
divide(divide(divide(X1,X2),zero),divide(divide(X1,divide(X2,X3)),X2)) = zero,
inference(orient,[status(thm)],[t26]) ).
cnf(t16,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t59,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t69,plain,
true = less_equal(divide(divide(X1,c),d),divide(divide(X1,identity),c)),
inference(cp,[status(thm)],[t59,t45]) ).
cnf(f6,axiom,
less_equal(X,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
fof(f6_nnf,plain,
! [X] : less_equal(X,identity),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] : less_equal(X,identity),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
less_equal(X0,identity),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
less_equal(X0,identity) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t0,plain,
divide(X1,identity) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi6]) ).
cnf(t19,plain,
divide(X1,identity) = zero,
inference(orient,[status(thm)],[t0]) ).
cnf(t1918,plain,
true = less_equal(divide(divide(X1,c),d),divide(zero,c)),
inference(step,[status(thm)],[t69,t19]) ).
cnf(t1919,plain,
true = less_equal(divide(divide(X1,c),d),zero),
inference(step,[status(thm)],[t1918,t35]) ).
cnf(t190,plain,
less_equal(divide(divide(X1,c),d),zero) = true,
inference(orient,[status(thm)],[t1919]) ).
cnf(t191,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,c),d)),true,divide(divide(X1,c),d),zero),zero),
inference(cp,[status(thm)],[t18,t190]) ).
cnf(t1920,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,c),d)),true,divide(divide(X1,c),d),zero),
inference(step,[status(thm)],[t191,t17]) ).
cnf(t1921,plain,
zero = ifeq(true,true,divide(divide(X1,c),d),zero),
inference(step,[status(thm)],[t1920,t86]) ).
cnf(t1922,plain,
zero = divide(divide(X1,c),d),
inference(step,[status(thm)],[t1921,t17]) ).
cnf(t193,plain,
divide(divide(X1,c),d) = zero,
inference(orient,[status(thm)],[t1922]) ).
cnf(t197,plain,
true = less_equal(divide(divide(X1,d),divide(c,d)),zero),
inference(cp,[status(thm)],[t59,t193]) ).
cnf(t341,plain,
less_equal(divide(divide(X1,d),divide(c,d)),zero) = true,
inference(orient,[status(thm)],[t197]) ).
cnf(t342,plain,
zero = ifeq(true,true,divide(divide(X1,d),divide(c,d)),zero),
inference(cp,[status(thm)],[t236,t341]) ).
cnf(t1946,plain,
zero = divide(divide(X1,d),divide(c,d)),
inference(step,[status(thm)],[t342,t17]) ).
cnf(t348,plain,
divide(divide(X1,d),divide(c,d)) = zero,
inference(orient,[status(thm)],[t1946]) ).
cnf(t357,plain,
zero = divide(divide(divide(divide(X1,d),c),zero),divide(zero,c)),
inference(cp,[status(thm)],[t255,t348]) ).
cnf(t1962,plain,
zero = divide(divide(divide(divide(X1,d),c),zero),zero),
inference(step,[status(thm)],[t357,t35]) ).
cnf(t468,plain,
divide(divide(divide(divide(X1,d),c),zero),zero) = zero,
inference(orient,[status(thm)],[t1962]) ).
cnf(t470,plain,
true = ifeq(zero,zero,less_equal(divide(divide(divide(X1,d),c),zero),zero),true),
inference(cp,[status(thm)],[t89,t468]) ).
cnf(t1969,plain,
true = less_equal(divide(divide(divide(X1,d),c),zero),zero),
inference(step,[status(thm)],[t470,t17]) ).
cnf(t518,plain,
less_equal(divide(divide(divide(X1,d),c),zero),zero) = true,
inference(orient,[status(thm)],[t1969]) ).
cnf(t519,plain,
zero = ifeq(true,true,divide(divide(divide(X1,d),c),zero),zero),
inference(cp,[status(thm)],[t236,t518]) ).
cnf(t1970,plain,
zero = divide(divide(divide(X1,d),c),zero),
inference(step,[status(thm)],[t519,t17]) ).
cnf(t523,plain,
divide(divide(divide(X1,d),c),zero) = zero,
inference(orient,[status(thm)],[t1970]) ).
cnf(t525,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,d),c),zero),true),
inference(cp,[status(thm)],[t89,t523]) ).
cnf(t1971,plain,
true = less_equal(divide(divide(X1,d),c),zero),
inference(step,[status(thm)],[t525,t17]) ).
cnf(t533,plain,
less_equal(divide(divide(X1,d),c),zero) = true,
inference(orient,[status(thm)],[t1971]) ).
cnf(t534,plain,
zero = ifeq(true,true,divide(divide(X1,d),c),zero),
inference(cp,[status(thm)],[t236,t533]) ).
cnf(t1972,plain,
zero = divide(divide(X1,d),c),
inference(step,[status(thm)],[t534,t17]) ).
cnf(t538,plain,
divide(divide(X1,d),c) = zero,
inference(orient,[status(thm)],[t1972]) ).
cnf(t1464,plain,
zero = divide(divide(divide(divide(X1,d),X2),divide(zero,X2)),divide(divide(c,X2),divide(divide(divide(X1,d),c),X2))),
inference(cp,[status(thm)],[t1422,t538]) ).
cnf(t2099,plain,
zero = divide(divide(divide(divide(X1,d),X2),zero),divide(divide(c,X2),divide(divide(divide(X1,d),c),X2))),
inference(step,[status(thm)],[t1464,t35]) ).
cnf(t2100,plain,
zero = divide(divide(divide(X1,d),X2),divide(divide(c,X2),divide(divide(divide(X1,d),c),X2))),
inference(step,[status(thm)],[t2099,t1123]) ).
cnf(t2101,plain,
zero = divide(divide(divide(X1,d),X2),divide(divide(c,X2),divide(zero,X2))),
inference(step,[status(thm)],[t2100,t538]) ).
cnf(t2102,plain,
zero = divide(divide(divide(X1,d),X2),divide(divide(c,X2),zero)),
inference(step,[status(thm)],[t2101,t35]) ).
cnf(t2103,plain,
zero = divide(divide(divide(X1,d),X2),divide(c,X2)),
inference(step,[status(thm)],[t2102,t1123]) ).
cnf(t1737,plain,
divide(divide(divide(X1,d),X2),divide(c,X2)) = zero,
inference(orient,[status(thm)],[t2103]) ).
cnf(t71,plain,
true = less_equal(divide(divide(X1,a),b),divide(divide(X1,identity),a)),
inference(cp,[status(thm)],[t59,t41]) ).
cnf(t1930,plain,
true = less_equal(divide(divide(X1,a),b),divide(zero,a)),
inference(step,[status(thm)],[t71,t19]) ).
cnf(t1931,plain,
true = less_equal(divide(divide(X1,a),b),zero),
inference(step,[status(thm)],[t1930,t35]) ).
cnf(t220,plain,
less_equal(divide(divide(X1,a),b),zero) = true,
inference(orient,[status(thm)],[t1931]) ).
cnf(t221,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,a),b)),true,divide(divide(X1,a),b),zero),zero),
inference(cp,[status(thm)],[t18,t220]) ).
cnf(t1932,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,a),b)),true,divide(divide(X1,a),b),zero),
inference(step,[status(thm)],[t221,t17]) ).
cnf(t1933,plain,
zero = ifeq(true,true,divide(divide(X1,a),b),zero),
inference(step,[status(thm)],[t1932,t86]) ).
cnf(t1934,plain,
zero = divide(divide(X1,a),b),
inference(step,[status(thm)],[t1933,t17]) ).
cnf(t223,plain,
divide(divide(X1,a),b) = zero,
inference(orient,[status(thm)],[t1934]) ).
cnf(t227,plain,
true = less_equal(divide(divide(X1,b),divide(a,b)),zero),
inference(cp,[status(thm)],[t59,t223]) ).
cnf(t415,plain,
less_equal(divide(divide(X1,b),divide(a,b)),zero) = true,
inference(orient,[status(thm)],[t227]) ).
cnf(t416,plain,
true = less_equal(divide(c,divide(a,b)),zero),
inference(cp,[status(thm)],[t415,t37]) ).
cnf(t423,plain,
less_equal(divide(c,divide(a,b)),zero) = true,
inference(orient,[status(thm)],[t416]) ).
cnf(t424,plain,
zero = ifeq(true,true,divide(c,divide(a,b)),zero),
inference(cp,[status(thm)],[t236,t423]) ).
cnf(t1955,plain,
zero = divide(c,divide(a,b)),
inference(step,[status(thm)],[t424,t17]) ).
cnf(t430,plain,
divide(c,divide(a,b)) = zero,
inference(orient,[status(thm)],[t1955]) ).
cnf(t432,plain,
true = ifeq(zero,zero,less_equal(c,divide(a,b)),true),
inference(cp,[status(thm)],[t89,t430]) ).
cnf(t1956,plain,
true = less_equal(c,divide(a,b)),
inference(step,[status(thm)],[t432,t17]) ).
cnf(t439,plain,
less_equal(c,divide(a,b)) = true,
inference(orient,[status(thm)],[t1956]) ).
cnf(t440,plain,
divide(a,b) = ifeq(true,true,ifeq(less_equal(divide(a,b),c),true,c,divide(a,b)),divide(a,b)),
inference(cp,[status(thm)],[t18,t439]) ).
cnf(t1957,plain,
divide(a,b) = ifeq(less_equal(divide(a,b),c),true,c,divide(a,b)),
inference(step,[status(thm)],[t440,t17]) ).
cnf(t70,plain,
true = less_equal(divide(divide(X1,b),c),divide(divide(X1,identity),b)),
inference(cp,[status(thm)],[t59,t37]) ).
cnf(t1924,plain,
true = less_equal(divide(divide(X1,b),c),divide(zero,b)),
inference(step,[status(thm)],[t70,t19]) ).
cnf(t1925,plain,
true = less_equal(divide(divide(X1,b),c),zero),
inference(step,[status(thm)],[t1924,t35]) ).
cnf(t205,plain,
less_equal(divide(divide(X1,b),c),zero) = true,
inference(orient,[status(thm)],[t1925]) ).
cnf(t206,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,b),c)),true,divide(divide(X1,b),c),zero),zero),
inference(cp,[status(thm)],[t18,t205]) ).
cnf(t1926,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,b),c)),true,divide(divide(X1,b),c),zero),
inference(step,[status(thm)],[t206,t17]) ).
cnf(t1927,plain,
zero = ifeq(true,true,divide(divide(X1,b),c),zero),
inference(step,[status(thm)],[t1926,t86]) ).
cnf(t1928,plain,
zero = divide(divide(X1,b),c),
inference(step,[status(thm)],[t1927,t17]) ).
cnf(t208,plain,
divide(divide(X1,b),c) = zero,
inference(orient,[status(thm)],[t1928]) ).
cnf(t210,plain,
true = ifeq(zero,zero,less_equal(divide(X1,b),c),true),
inference(cp,[status(thm)],[t89,t208]) ).
cnf(t1929,plain,
true = less_equal(divide(X1,b),c),
inference(step,[status(thm)],[t210,t17]) ).
cnf(t217,plain,
less_equal(divide(X1,b),c) = true,
inference(orient,[status(thm)],[t1929]) ).
cnf(t1958,plain,
divide(a,b) = ifeq(true,true,c,divide(a,b)),
inference(step,[status(thm)],[t1957,t217]) ).
cnf(t1959,plain,
divide(a,b) = c,
inference(step,[status(thm)],[t1958,t17]) ).
cnf(t442,plain,
divide(a,b) = c,
inference(orient,[status(thm)],[t1959]) ).
cnf(t443,plain,
zero = divide(c,a),
inference(cp,[status(thm)],[t20,t442]) ).
cnf(t453,plain,
divide(c,a) = zero,
inference(orient,[status(thm)],[t443]) ).
cnf(t1741,plain,
zero = divide(divide(divide(X1,d),a),zero),
inference(cp,[status(thm)],[t1737,t453]) ).
cnf(t2104,plain,
zero = divide(divide(X1,d),a),
inference(step,[status(thm)],[t1741,t1123]) ).
cnf(t1757,plain,
divide(divide(X1,d),a) = zero,
inference(orient,[status(thm)],[t2104]) ).
cnf(t1766,plain,
zero = divide(divide(divide(X1,a),divide(d,a)),zero),
inference(cp,[status(thm)],[t23,t1757]) ).
cnf(t2107,plain,
zero = divide(divide(X1,a),divide(d,a)),
inference(step,[status(thm)],[t1766,t1123]) ).
cnf(t1788,plain,
divide(divide(X1,a),divide(d,a)) = zero,
inference(orient,[status(thm)],[t2107]) ).
cnf(t1789,plain,
zero = divide(b,divide(d,a)),
inference(cp,[status(thm)],[t1788,t41]) ).
cnf(t1805,plain,
divide(b,divide(d,a)) = zero,
inference(orient,[status(thm)],[t1789]) ).
cnf(t1809,plain,
true = ifeq(zero,zero,less_equal(b,divide(d,a)),true),
inference(cp,[status(thm)],[t89,t1805]) ).
cnf(t2109,plain,
true = less_equal(b,divide(d,a)),
inference(step,[status(thm)],[t1809,t17]) ).
cnf(t1834,plain,
less_equal(b,divide(d,a)) = true,
inference(orient,[status(thm)],[t2109]) ).
cnf(t1835,plain,
divide(d,a) = ifeq(true,true,ifeq(less_equal(divide(d,a),b),true,b,divide(d,a)),divide(d,a)),
inference(cp,[status(thm)],[t18,t1834]) ).
cnf(t2110,plain,
divide(d,a) = ifeq(less_equal(divide(d,a),b),true,b,divide(d,a)),
inference(step,[status(thm)],[t1835,t17]) ).
cnf(t212,plain,
true = less_equal(divide(divide(X1,c),divide(b,c)),zero),
inference(cp,[status(thm)],[t59,t208]) ).
cnf(t362,plain,
less_equal(divide(divide(X1,c),divide(b,c)),zero) = true,
inference(orient,[status(thm)],[t212]) ).
cnf(t363,plain,
true = less_equal(divide(d,divide(b,c)),zero),
inference(cp,[status(thm)],[t362,t45]) ).
cnf(t370,plain,
less_equal(divide(d,divide(b,c)),zero) = true,
inference(orient,[status(thm)],[t363]) ).
cnf(t371,plain,
zero = ifeq(true,true,divide(d,divide(b,c)),zero),
inference(cp,[status(thm)],[t236,t370]) ).
cnf(t1948,plain,
zero = divide(d,divide(b,c)),
inference(step,[status(thm)],[t371,t17]) ).
cnf(t377,plain,
divide(d,divide(b,c)) = zero,
inference(orient,[status(thm)],[t1948]) ).
cnf(t379,plain,
true = ifeq(zero,zero,less_equal(d,divide(b,c)),true),
inference(cp,[status(thm)],[t89,t377]) ).
cnf(t1949,plain,
true = less_equal(d,divide(b,c)),
inference(step,[status(thm)],[t379,t17]) ).
cnf(t386,plain,
less_equal(d,divide(b,c)) = true,
inference(orient,[status(thm)],[t1949]) ).
cnf(t387,plain,
divide(b,c) = ifeq(true,true,ifeq(less_equal(divide(b,c),d),true,d,divide(b,c)),divide(b,c)),
inference(cp,[status(thm)],[t18,t386]) ).
cnf(t1950,plain,
divide(b,c) = ifeq(less_equal(divide(b,c),d),true,d,divide(b,c)),
inference(step,[status(thm)],[t387,t17]) ).
cnf(t195,plain,
true = ifeq(zero,zero,less_equal(divide(X1,c),d),true),
inference(cp,[status(thm)],[t89,t193]) ).
cnf(t1923,plain,
true = less_equal(divide(X1,c),d),
inference(step,[status(thm)],[t195,t17]) ).
cnf(t202,plain,
less_equal(divide(X1,c),d) = true,
inference(orient,[status(thm)],[t1923]) ).
cnf(t1951,plain,
divide(b,c) = ifeq(true,true,d,divide(b,c)),
inference(step,[status(thm)],[t1950,t202]) ).
cnf(t1952,plain,
divide(b,c) = d,
inference(step,[status(thm)],[t1951,t17]) ).
cnf(t389,plain,
divide(b,c) = d,
inference(orient,[status(thm)],[t1952]) ).
cnf(t390,plain,
zero = divide(d,b),
inference(cp,[status(thm)],[t20,t389]) ).
cnf(t400,plain,
divide(d,b) = zero,
inference(orient,[status(thm)],[t390]) ).
cnf(t404,plain,
true = less_equal(divide(divide(d,X1),divide(b,X1)),divide(zero,X1)),
inference(cp,[status(thm)],[t59,t400]) ).
cnf(t1963,plain,
true = less_equal(divide(divide(d,X1),divide(b,X1)),zero),
inference(step,[status(thm)],[t404,t35]) ).
cnf(t476,plain,
less_equal(divide(divide(d,X1),divide(b,X1)),zero) = true,
inference(orient,[status(thm)],[t1963]) ).
cnf(t477,plain,
zero = ifeq(true,true,divide(divide(d,X1),divide(b,X1)),zero),
inference(cp,[status(thm)],[t236,t476]) ).
cnf(t1964,plain,
zero = divide(divide(d,X1),divide(b,X1)),
inference(step,[status(thm)],[t477,t17]) ).
cnf(t483,plain,
divide(divide(d,X1),divide(b,X1)) = zero,
inference(orient,[status(thm)],[t1964]) ).
cnf(t492,plain,
zero = divide(divide(divide(divide(d,X1),b),zero),divide(zero,b)),
inference(cp,[status(thm)],[t255,t483]) ).
cnf(t1974,plain,
zero = divide(divide(divide(divide(d,X1),b),zero),zero),
inference(step,[status(thm)],[t492,t35]) ).
cnf(t551,plain,
divide(divide(divide(divide(d,X1),b),zero),zero) = zero,
inference(orient,[status(thm)],[t1974]) ).
cnf(t553,plain,
true = ifeq(zero,zero,less_equal(divide(divide(divide(d,X1),b),zero),zero),true),
inference(cp,[status(thm)],[t89,t551]) ).
cnf(t1982,plain,
true = less_equal(divide(divide(divide(d,X1),b),zero),zero),
inference(step,[status(thm)],[t553,t17]) ).
cnf(t628,plain,
less_equal(divide(divide(divide(d,X1),b),zero),zero) = true,
inference(orient,[status(thm)],[t1982]) ).
cnf(t629,plain,
zero = ifeq(true,true,divide(divide(divide(d,X1),b),zero),zero),
inference(cp,[status(thm)],[t236,t628]) ).
cnf(t1983,plain,
zero = divide(divide(divide(d,X1),b),zero),
inference(step,[status(thm)],[t629,t17]) ).
cnf(t633,plain,
divide(divide(divide(d,X1),b),zero) = zero,
inference(orient,[status(thm)],[t1983]) ).
cnf(t635,plain,
true = ifeq(zero,zero,less_equal(divide(divide(d,X1),b),zero),true),
inference(cp,[status(thm)],[t89,t633]) ).
cnf(t1984,plain,
true = less_equal(divide(divide(d,X1),b),zero),
inference(step,[status(thm)],[t635,t17]) ).
cnf(t644,plain,
less_equal(divide(divide(d,X1),b),zero) = true,
inference(orient,[status(thm)],[t1984]) ).
cnf(t645,plain,
zero = ifeq(true,true,divide(divide(d,X1),b),zero),
inference(cp,[status(thm)],[t236,t644]) ).
cnf(t1985,plain,
zero = divide(divide(d,X1),b),
inference(step,[status(thm)],[t645,t17]) ).
cnf(t649,plain,
divide(divide(d,X1),b) = zero,
inference(orient,[status(thm)],[t1985]) ).
cnf(t651,plain,
true = ifeq(zero,zero,less_equal(divide(d,X1),b),true),
inference(cp,[status(thm)],[t89,t649]) ).
cnf(t1986,plain,
true = less_equal(divide(d,X1),b),
inference(step,[status(thm)],[t651,t17]) ).
cnf(t658,plain,
less_equal(divide(d,X1),b) = true,
inference(orient,[status(thm)],[t1986]) ).
cnf(t2111,plain,
divide(d,a) = ifeq(true,true,b,divide(d,a)),
inference(step,[status(thm)],[t2110,t658]) ).
cnf(t2112,plain,
divide(d,a) = b,
inference(step,[status(thm)],[t2111,t17]) ).
cnf(t1837,plain,
divide(d,a) = b,
inference(orient,[status(thm)],[t2112]) ).
cnf(t1843,plain,
true = less_equal(b,d),
inference(cp,[status(thm)],[t52,t1837]) ).
cnf(t1867,plain,
less_equal(b,d) = true,
inference(orient,[status(thm)],[t1843]) ).
cnf(t1868,plain,
d = ifeq(true,true,ifeq(less_equal(d,b),true,b,d),d),
inference(cp,[status(thm)],[t18,t1867]) ).
cnf(t2117,plain,
d = ifeq(less_equal(d,b),true,b,d),
inference(step,[status(thm)],[t1868,t17]) ).
cnf(t393,plain,
true = less_equal(d,b),
inference(cp,[status(thm)],[t52,t389]) ).
cnf(t408,plain,
less_equal(d,b) = true,
inference(orient,[status(thm)],[t393]) ).
cnf(t2118,plain,
d = ifeq(true,true,b,d),
inference(step,[status(thm)],[t2117,t408]) ).
cnf(t2119,plain,
d = b,
inference(step,[status(thm)],[t2118,t17]) ).
cnf(t1872,plain,
b = d,
inference(orient,[status(thm)],[t2119]) ).
cnf(t2124,plain,
ifeq(d,d,false,true) = true,
inference(step,[status(thm)],[t93,t1872]) ).
cnf(t2125,plain,
false = true,
inference(step,[status(thm)],[t2124,t17]) ).
cnf(t1877,plain,
false = true,
inference(rw,[status(thm)],[t2125]) ).
cnf(t1890,plain,
false = true,
inference(orient,[status(thm)],[t1877]) ).
cnf(f11,negated_conjecture,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_b_equals_d) ).
fof(f11_nnf,plain,
b != d,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
b != d,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
b != d,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7,c11]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1890]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN009-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n009.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 : Wed Sep 23 16:15:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.16/1.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.16/1.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------