%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HEN010-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 : n014.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:10 PM UTC 2026
% Result : Unsatisfiable 7.17s 1.56s
% Output : Proof 7.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 12
% Syntax : Number of formulae : 237 ( 225 unt; 0 def)
% Number of atoms : 253 ( 220 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 : 5 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-4 aty)
% Number of variables : 178 ( 51 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
sFlat0 = divide(identity,a),
introduced(definition) ).
cnf(t16,plain,
divide(identity,a) = sFlat0,
inference(orient,[status(thm)],[t8]) ).
cnf(t9,axiom,
sFlat1 = divide(identity,divide(identity,a)),
introduced(definition) ).
cnf(t14,plain,
divide(identity,divide(identity,a)) = sFlat1,
inference(orient,[status(thm)],[t9]) ).
cnf(t836,plain,
divide(identity,sFlat0) = sFlat1,
inference(step,[status(thm)],[t14,t16]) ).
cnf(t17,plain,
divide(identity,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t836]) ).
cnf(t45,plain,
divide(identity,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t17]) ).
cnf(t10,axiom,
sFlat2 = divide(divide(identity,a),divide(identity,divide(identity,a))),
introduced(definition) ).
cnf(t13,plain,
divide(divide(identity,a),divide(identity,divide(identity,a))) = sFlat2,
inference(orient,[status(thm)],[t10]) ).
cnf(t835,plain,
divide(divide(identity,a),sFlat1) = sFlat2,
inference(step,[status(thm)],[t13,t14]) ).
cnf(t15,plain,
divide(divide(identity,a),sFlat1) = sFlat2,
inference(rw,[status(thm)],[t835]) ).
cnf(t839,plain,
divide(sFlat0,sFlat1) = sFlat2,
inference(step,[status(thm)],[t15,t16]) ).
cnf(t55,plain,
divide(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t839]) ).
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(t6,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t12,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t6]) ).
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(t3,plain,
less_equal(divide(X1,X2),X1) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t21,plain,
less_equal(divide(X1,X2),X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t23,plain,
divide(X1,X2) = ifeq(less_equal(X1,divide(X1,X2)),true,ifeq(true,true,X1,divide(X1,X2)),divide(X1,X2)),
inference(cp,[status(thm)],[t12,t21]) ).
cnf(t2,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t866,plain,
divide(X1,X2) = ifeq(less_equal(X1,divide(X1,X2)),true,X1,divide(X1,X2)),
inference(step,[status(thm)],[t23,t11]) ).
cnf(t206,plain,
ifeq(less_equal(X1,divide(X1,X2)),true,X1,divide(X1,X2)) = divide(X1,X2),
inference(orient,[status(thm)],[t866]) ).
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(t4,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t33,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(orient,[status(thm)],[t4]) ).
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(t1,plain,
less_equal(zero,X1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t30,plain,
less_equal(zero,X1) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t32,plain,
zero = ifeq(less_equal(X1,zero),true,ifeq(true,true,X1,zero),zero),
inference(cp,[status(thm)],[t12,t30]) ).
cnf(t845,plain,
zero = ifeq(less_equal(X1,zero),true,X1,zero),
inference(step,[status(thm)],[t32,t11]) ).
cnf(t77,plain,
ifeq(less_equal(X1,zero),true,X1,zero) = zero,
inference(orient,[status(thm)],[t845]) ).
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(t7,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t24,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t28,plain,
divide(divide(X1,X2),X3) = ifeq(true,true,ifeq(less_equal(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),true,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)),divide(divide(X1,X2),X3)),
inference(cp,[status(thm)],[t12,t24]) ).
cnf(t905,plain,
divide(divide(X1,X2),X3) = ifeq(less_equal(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),true,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)),
inference(step,[status(thm)],[t28,t11]) ).
cnf(t448,plain,
ifeq(less_equal(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),true,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)) = divide(divide(X1,X2),X3),
inference(orient,[status(thm)],[t905]) ).
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(t5,plain,
ifeq(less_equal(X1,X2),true,divide(X1,X2),zero) = zero,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t39,plain,
ifeq(less_equal(X1,X2),true,divide(X1,X2),zero) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t25,plain,
true = less_equal(divide(sFlat0,divide(X1,a)),divide(divide(identity,X1),a)),
inference(cp,[status(thm)],[t24,t16]) ).
cnf(t141,plain,
less_equal(divide(sFlat0,divide(X1,a)),divide(divide(identity,X1),a)) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t26,plain,
true = less_equal(divide(divide(X1,a),sFlat0),divide(divide(X1,identity),a)),
inference(cp,[status(thm)],[t24,t16]) ).
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(t0,plain,
less_equal(X1,identity) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t18,plain,
less_equal(X1,identity) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t40,plain,
zero = ifeq(true,true,divide(X1,identity),zero),
inference(cp,[status(thm)],[t39,t18]) ).
cnf(t837,plain,
zero = divide(X1,identity),
inference(step,[status(thm)],[t40,t11]) ).
cnf(t51,plain,
divide(X1,identity) = zero,
inference(orient,[status(thm)],[t837]) ).
cnf(t868,plain,
true = less_equal(divide(divide(X1,a),sFlat0),divide(zero,a)),
inference(step,[status(thm)],[t26,t51]) ).
cnf(t41,plain,
zero = ifeq(true,true,divide(zero,X1),zero),
inference(cp,[status(thm)],[t39,t30]) ).
cnf(t838,plain,
zero = divide(zero,X1),
inference(step,[status(thm)],[t41,t11]) ).
cnf(t53,plain,
divide(zero,X1) = zero,
inference(orient,[status(thm)],[t838]) ).
cnf(t869,plain,
true = less_equal(divide(divide(X1,a),sFlat0),zero),
inference(step,[status(thm)],[t868,t53]) ).
cnf(t221,plain,
less_equal(divide(divide(X1,a),sFlat0),zero) = true,
inference(orient,[status(thm)],[t869]) ).
cnf(t222,plain,
zero = ifeq(true,true,divide(divide(X1,a),sFlat0),zero),
inference(cp,[status(thm)],[t77,t221]) ).
cnf(t870,plain,
zero = divide(divide(X1,a),sFlat0),
inference(step,[status(thm)],[t222,t11]) ).
cnf(t228,plain,
divide(divide(X1,a),sFlat0) = zero,
inference(orient,[status(thm)],[t870]) ).
cnf(t232,plain,
true = less_equal(divide(divide(X1,sFlat0),divide(a,sFlat0)),zero),
inference(cp,[status(thm)],[t24,t228]) ).
cnf(t237,plain,
less_equal(divide(divide(X1,sFlat0),divide(a,sFlat0)),zero) = true,
inference(orient,[status(thm)],[t232]) ).
cnf(t238,plain,
true = less_equal(divide(sFlat1,divide(a,sFlat0)),zero),
inference(cp,[status(thm)],[t237,t45]) ).
cnf(t245,plain,
less_equal(divide(sFlat1,divide(a,sFlat0)),zero) = true,
inference(orient,[status(thm)],[t238]) ).
cnf(t246,plain,
zero = ifeq(true,true,divide(sFlat1,divide(a,sFlat0)),zero),
inference(cp,[status(thm)],[t77,t245]) ).
cnf(t872,plain,
zero = divide(sFlat1,divide(a,sFlat0)),
inference(step,[status(thm)],[t246,t11]) ).
cnf(t252,plain,
divide(sFlat1,divide(a,sFlat0)) = zero,
inference(orient,[status(thm)],[t872]) ).
cnf(t463,plain,
divide(divide(sFlat1,divide(a,sFlat0)),X1) = ifeq(less_equal(divide(zero,X1),divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1))),true,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),divide(divide(sFlat1,divide(a,sFlat0)),X1)),
inference(cp,[status(thm)],[t448,t252]) ).
cnf(t920,plain,
divide(zero,X1) = ifeq(less_equal(divide(zero,X1),divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1))),true,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),divide(divide(sFlat1,divide(a,sFlat0)),X1)),
inference(step,[status(thm)],[t463,t252]) ).
cnf(t921,plain,
zero = ifeq(less_equal(divide(zero,X1),divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1))),true,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),divide(divide(sFlat1,divide(a,sFlat0)),X1)),
inference(step,[status(thm)],[t920,t53]) ).
cnf(t922,plain,
zero = ifeq(less_equal(zero,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1))),true,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),divide(divide(sFlat1,divide(a,sFlat0)),X1)),
inference(step,[status(thm)],[t921,t53]) ).
cnf(t923,plain,
zero = ifeq(true,true,divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),divide(divide(sFlat1,divide(a,sFlat0)),X1)),
inference(step,[status(thm)],[t922,t30]) ).
cnf(t924,plain,
zero = divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)),
inference(step,[status(thm)],[t923,t11]) ).
cnf(t620,plain,
divide(divide(sFlat1,X1),divide(divide(a,sFlat0),X1)) = zero,
inference(orient,[status(thm)],[t924]) ).
cnf(t42,plain,
zero = ifeq(true,true,divide(divide(X1,X2),X1),zero),
inference(cp,[status(thm)],[t39,t21]) ).
cnf(t841,plain,
zero = divide(divide(X1,X2),X1),
inference(step,[status(thm)],[t42,t11]) ).
cnf(t70,plain,
divide(divide(X1,X2),X1) = zero,
inference(orient,[status(thm)],[t841]) ).
cnf(t622,plain,
zero = divide(divide(sFlat1,a),zero),
inference(cp,[status(thm)],[t620,t70]) ).
cnf(t636,plain,
divide(divide(sFlat1,a),zero) = zero,
inference(orient,[status(thm)],[t622]) ).
cnf(t638,plain,
true = ifeq(zero,zero,less_equal(divide(sFlat1,a),zero),true),
inference(cp,[status(thm)],[t33,t636]) ).
cnf(t925,plain,
true = less_equal(divide(sFlat1,a),zero),
inference(step,[status(thm)],[t638,t11]) ).
cnf(t648,plain,
less_equal(divide(sFlat1,a),zero) = true,
inference(orient,[status(thm)],[t925]) ).
cnf(t649,plain,
zero = ifeq(true,true,divide(sFlat1,a),zero),
inference(cp,[status(thm)],[t77,t648]) ).
cnf(t926,plain,
zero = divide(sFlat1,a),
inference(step,[status(thm)],[t649,t11]) ).
cnf(t653,plain,
divide(sFlat1,a) = zero,
inference(orient,[status(thm)],[t926]) ).
cnf(t657,plain,
true = less_equal(divide(sFlat0,zero),divide(divide(identity,sFlat1),a)),
inference(cp,[status(thm)],[t141,t653]) ).
cnf(t52,plain,
true = less_equal(divide(divide(X1,X2),divide(identity,X2)),divide(zero,X2)),
inference(cp,[status(thm)],[t24,t51]) ).
cnf(t898,plain,
true = less_equal(divide(divide(X1,X2),divide(identity,X2)),zero),
inference(step,[status(thm)],[t52,t53]) ).
cnf(t411,plain,
less_equal(divide(divide(X1,X2),divide(identity,X2)),zero) = true,
inference(orient,[status(thm)],[t898]) ).
cnf(t412,plain,
true = less_equal(divide(sFlat2,divide(identity,sFlat1)),zero),
inference(cp,[status(thm)],[t411,t55]) ).
cnf(t419,plain,
less_equal(divide(sFlat2,divide(identity,sFlat1)),zero) = true,
inference(orient,[status(thm)],[t412]) ).
cnf(t420,plain,
zero = ifeq(true,true,divide(sFlat2,divide(identity,sFlat1)),zero),
inference(cp,[status(thm)],[t77,t419]) ).
cnf(t899,plain,
zero = divide(sFlat2,divide(identity,sFlat1)),
inference(step,[status(thm)],[t420,t11]) ).
cnf(t426,plain,
divide(sFlat2,divide(identity,sFlat1)) = zero,
inference(orient,[status(thm)],[t899]) ).
cnf(t428,plain,
true = ifeq(zero,zero,less_equal(sFlat2,divide(identity,sFlat1)),true),
inference(cp,[status(thm)],[t33,t426]) ).
cnf(t900,plain,
true = less_equal(sFlat2,divide(identity,sFlat1)),
inference(step,[status(thm)],[t428,t11]) ).
cnf(t431,plain,
less_equal(sFlat2,divide(identity,sFlat1)) = true,
inference(orient,[status(thm)],[t900]) ).
cnf(t432,plain,
divide(identity,sFlat1) = ifeq(true,true,ifeq(less_equal(divide(identity,sFlat1),sFlat2),true,sFlat2,divide(identity,sFlat1)),divide(identity,sFlat1)),
inference(cp,[status(thm)],[t12,t431]) ).
cnf(t901,plain,
divide(identity,sFlat1) = ifeq(less_equal(divide(identity,sFlat1),sFlat2),true,sFlat2,divide(identity,sFlat1)),
inference(step,[status(thm)],[t432,t11]) ).
cnf(t49,plain,
true = less_equal(divide(divide(X1,sFlat0),sFlat1),divide(divide(X1,identity),sFlat0)),
inference(cp,[status(thm)],[t24,t45]) ).
cnf(t889,plain,
true = less_equal(divide(divide(X1,sFlat0),sFlat1),divide(zero,sFlat0)),
inference(step,[status(thm)],[t49,t51]) ).
cnf(t890,plain,
true = less_equal(divide(divide(X1,sFlat0),sFlat1),zero),
inference(step,[status(thm)],[t889,t53]) ).
cnf(t357,plain,
less_equal(divide(divide(X1,sFlat0),sFlat1),zero) = true,
inference(orient,[status(thm)],[t890]) ).
cnf(t358,plain,
zero = ifeq(true,true,divide(divide(X1,sFlat0),sFlat1),zero),
inference(cp,[status(thm)],[t77,t357]) ).
cnf(t891,plain,
zero = divide(divide(X1,sFlat0),sFlat1),
inference(step,[status(thm)],[t358,t11]) ).
cnf(t364,plain,
divide(divide(X1,sFlat0),sFlat1) = zero,
inference(orient,[status(thm)],[t891]) ).
cnf(t368,plain,
true = less_equal(divide(divide(X1,sFlat1),divide(sFlat0,sFlat1)),zero),
inference(cp,[status(thm)],[t24,t364]) ).
cnf(t893,plain,
true = less_equal(divide(divide(X1,sFlat1),sFlat2),zero),
inference(step,[status(thm)],[t368,t55]) ).
cnf(t373,plain,
less_equal(divide(divide(X1,sFlat1),sFlat2),zero) = true,
inference(orient,[status(thm)],[t893]) ).
cnf(t374,plain,
zero = ifeq(true,true,divide(divide(X1,sFlat1),sFlat2),zero),
inference(cp,[status(thm)],[t77,t373]) ).
cnf(t894,plain,
zero = divide(divide(X1,sFlat1),sFlat2),
inference(step,[status(thm)],[t374,t11]) ).
cnf(t380,plain,
divide(divide(X1,sFlat1),sFlat2) = zero,
inference(orient,[status(thm)],[t894]) ).
cnf(t382,plain,
true = ifeq(zero,zero,less_equal(divide(X1,sFlat1),sFlat2),true),
inference(cp,[status(thm)],[t33,t380]) ).
cnf(t895,plain,
true = less_equal(divide(X1,sFlat1),sFlat2),
inference(step,[status(thm)],[t382,t11]) ).
cnf(t386,plain,
less_equal(divide(X1,sFlat1),sFlat2) = true,
inference(orient,[status(thm)],[t895]) ).
cnf(t902,plain,
divide(identity,sFlat1) = ifeq(true,true,sFlat2,divide(identity,sFlat1)),
inference(step,[status(thm)],[t901,t386]) ).
cnf(t903,plain,
divide(identity,sFlat1) = sFlat2,
inference(step,[status(thm)],[t902,t11]) ).
cnf(t434,plain,
divide(identity,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t903]) ).
cnf(t929,plain,
true = less_equal(divide(sFlat0,zero),divide(sFlat2,a)),
inference(step,[status(thm)],[t657,t434]) ).
cnf(t693,plain,
less_equal(divide(sFlat0,zero),divide(sFlat2,a)) = true,
inference(orient,[status(thm)],[t929]) ).
cnf(t694,plain,
zero = ifeq(true,true,divide(divide(sFlat0,zero),divide(sFlat2,a)),zero),
inference(cp,[status(thm)],[t39,t693]) ).
cnf(t947,plain,
zero = divide(divide(sFlat0,zero),divide(sFlat2,a)),
inference(step,[status(thm)],[t694,t11]) ).
cnf(t760,plain,
divide(divide(sFlat0,zero),divide(sFlat2,a)) = zero,
inference(orient,[status(thm)],[t947]) ).
cnf(t764,plain,
divide(divide(sFlat0,zero),divide(sFlat2,a)) = ifeq(less_equal(zero,divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a)))),true,divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a))),divide(divide(sFlat0,zero),divide(sFlat2,a))),
inference(cp,[status(thm)],[t448,t760]) ).
cnf(t949,plain,
zero = ifeq(less_equal(zero,divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a)))),true,divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a))),divide(divide(sFlat0,zero),divide(sFlat2,a))),
inference(step,[status(thm)],[t764,t760]) ).
cnf(t950,plain,
zero = ifeq(true,true,divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a))),divide(divide(sFlat0,zero),divide(sFlat2,a))),
inference(step,[status(thm)],[t949,t30]) ).
cnf(t951,plain,
zero = divide(divide(sFlat0,divide(sFlat2,a)),divide(zero,divide(sFlat2,a))),
inference(step,[status(thm)],[t950,t11]) ).
cnf(t952,plain,
zero = divide(divide(sFlat0,divide(sFlat2,a)),zero),
inference(step,[status(thm)],[t951,t53]) ).
cnf(t777,plain,
divide(divide(sFlat0,divide(sFlat2,a)),zero) = zero,
inference(orient,[status(thm)],[t952]) ).
cnf(t779,plain,
true = ifeq(zero,zero,less_equal(divide(sFlat0,divide(sFlat2,a)),zero),true),
inference(cp,[status(thm)],[t33,t777]) ).
cnf(t953,plain,
true = less_equal(divide(sFlat0,divide(sFlat2,a)),zero),
inference(step,[status(thm)],[t779,t11]) ).
cnf(t789,plain,
less_equal(divide(sFlat0,divide(sFlat2,a)),zero) = true,
inference(orient,[status(thm)],[t953]) ).
cnf(t790,plain,
zero = ifeq(true,true,divide(sFlat0,divide(sFlat2,a)),zero),
inference(cp,[status(thm)],[t77,t789]) ).
cnf(t954,plain,
zero = divide(sFlat0,divide(sFlat2,a)),
inference(step,[status(thm)],[t790,t11]) ).
cnf(t794,plain,
divide(sFlat0,divide(sFlat2,a)) = zero,
inference(orient,[status(thm)],[t954]) ).
cnf(t798,plain,
true = ifeq(zero,zero,less_equal(sFlat0,divide(sFlat2,a)),true),
inference(cp,[status(thm)],[t33,t794]) ).
cnf(t955,plain,
true = less_equal(sFlat0,divide(sFlat2,a)),
inference(step,[status(thm)],[t798,t11]) ).
cnf(t807,plain,
less_equal(sFlat0,divide(sFlat2,a)) = true,
inference(orient,[status(thm)],[t955]) ).
cnf(t808,plain,
divide(sFlat2,a) = ifeq(true,true,ifeq(less_equal(divide(sFlat2,a),sFlat0),true,sFlat0,divide(sFlat2,a)),divide(sFlat2,a)),
inference(cp,[status(thm)],[t12,t807]) ).
cnf(t956,plain,
divide(sFlat2,a) = ifeq(less_equal(divide(sFlat2,a),sFlat0),true,sFlat0,divide(sFlat2,a)),
inference(step,[status(thm)],[t808,t11]) ).
cnf(t56,plain,
true = less_equal(sFlat2,sFlat0),
inference(cp,[status(thm)],[t21,t55]) ).
cnf(t62,plain,
less_equal(sFlat2,sFlat0) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t63,plain,
zero = ifeq(true,true,divide(sFlat2,sFlat0),zero),
inference(cp,[status(thm)],[t39,t62]) ).
cnf(t840,plain,
zero = divide(sFlat2,sFlat0),
inference(step,[status(thm)],[t63,t11]) ).
cnf(t67,plain,
divide(sFlat2,sFlat0) = zero,
inference(orient,[status(thm)],[t840]) ).
cnf(t69,plain,
true = less_equal(divide(divide(sFlat2,X1),divide(sFlat0,X1)),divide(zero,X1)),
inference(cp,[status(thm)],[t24,t67]) ).
cnf(t848,plain,
true = less_equal(divide(divide(sFlat2,X1),divide(sFlat0,X1)),zero),
inference(step,[status(thm)],[t69,t53]) ).
cnf(t86,plain,
less_equal(divide(divide(sFlat2,X1),divide(sFlat0,X1)),zero) = true,
inference(orient,[status(thm)],[t848]) ).
cnf(t87,plain,
zero = ifeq(true,true,divide(divide(sFlat2,X1),divide(sFlat0,X1)),zero),
inference(cp,[status(thm)],[t77,t86]) ).
cnf(t849,plain,
zero = divide(divide(sFlat2,X1),divide(sFlat0,X1)),
inference(step,[status(thm)],[t87,t11]) ).
cnf(t93,plain,
divide(divide(sFlat2,X1),divide(sFlat0,X1)) = zero,
inference(orient,[status(thm)],[t849]) ).
cnf(t95,plain,
true = ifeq(zero,zero,less_equal(divide(sFlat2,X1),divide(sFlat0,X1)),true),
inference(cp,[status(thm)],[t33,t93]) ).
cnf(t850,plain,
true = less_equal(divide(sFlat2,X1),divide(sFlat0,X1)),
inference(step,[status(thm)],[t95,t11]) ).
cnf(t99,plain,
less_equal(divide(sFlat2,X1),divide(sFlat0,X1)) = true,
inference(orient,[status(thm)],[t850]) ).
cnf(t72,plain,
true = less_equal(divide(divide(X1,X1),divide(X2,X1)),zero),
inference(cp,[status(thm)],[t24,t70]) ).
cnf(t102,plain,
less_equal(divide(divide(X1,X1),divide(X2,X1)),zero) = true,
inference(orient,[status(thm)],[t72]) ).
cnf(t103,plain,
true = less_equal(divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t102,t70]) ).
cnf(t116,plain,
less_equal(divide(divide(X1,X1),zero),zero) = true,
inference(orient,[status(thm)],[t103]) ).
cnf(t117,plain,
zero = ifeq(true,true,divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t77,t116]) ).
cnf(t851,plain,
zero = divide(divide(X1,X1),zero),
inference(step,[status(thm)],[t117,t11]) ).
cnf(t123,plain,
divide(divide(X1,X1),zero) = zero,
inference(orient,[status(thm)],[t851]) ).
cnf(t125,plain,
true = ifeq(zero,zero,less_equal(divide(X1,X1),zero),true),
inference(cp,[status(thm)],[t33,t123]) ).
cnf(t852,plain,
true = less_equal(divide(X1,X1),zero),
inference(step,[status(thm)],[t125,t11]) ).
cnf(t129,plain,
less_equal(divide(X1,X1),zero) = true,
inference(orient,[status(thm)],[t852]) ).
cnf(t130,plain,
zero = ifeq(true,true,divide(X1,X1),zero),
inference(cp,[status(thm)],[t77,t129]) ).
cnf(t853,plain,
zero = divide(X1,X1),
inference(step,[status(thm)],[t130,t11]) ).
cnf(t134,plain,
divide(X1,X1) = zero,
inference(orient,[status(thm)],[t853]) ).
cnf(t142,plain,
true = less_equal(divide(sFlat0,zero),divide(divide(identity,a),a)),
inference(cp,[status(thm)],[t141,t134]) ).
cnf(t856,plain,
true = less_equal(divide(sFlat0,zero),divide(sFlat0,a)),
inference(step,[status(thm)],[t142,t16]) ).
cnf(t151,plain,
less_equal(divide(sFlat0,zero),divide(sFlat0,a)) = true,
inference(orient,[status(thm)],[t856]) ).
cnf(t152,plain,
zero = ifeq(true,true,divide(divide(sFlat0,zero),divide(sFlat0,a)),zero),
inference(cp,[status(thm)],[t39,t151]) ).
cnf(t857,plain,
zero = divide(divide(sFlat0,zero),divide(sFlat0,a)),
inference(step,[status(thm)],[t152,t11]) ).
cnf(t156,plain,
divide(divide(sFlat0,zero),divide(sFlat0,a)) = zero,
inference(orient,[status(thm)],[t857]) ).
cnf(t158,plain,
true = less_equal(divide(divide(sFlat0,divide(sFlat0,a)),divide(zero,divide(sFlat0,a))),zero),
inference(cp,[status(thm)],[t24,t156]) ).
cnf(t858,plain,
true = less_equal(divide(divide(sFlat0,divide(sFlat0,a)),zero),zero),
inference(step,[status(thm)],[t158,t53]) ).
cnf(t170,plain,
less_equal(divide(divide(sFlat0,divide(sFlat0,a)),zero),zero) = true,
inference(orient,[status(thm)],[t858]) ).
cnf(t171,plain,
zero = ifeq(true,true,divide(divide(sFlat0,divide(sFlat0,a)),zero),zero),
inference(cp,[status(thm)],[t77,t170]) ).
cnf(t859,plain,
zero = divide(divide(sFlat0,divide(sFlat0,a)),zero),
inference(step,[status(thm)],[t171,t11]) ).
cnf(t177,plain,
divide(divide(sFlat0,divide(sFlat0,a)),zero) = zero,
inference(orient,[status(thm)],[t859]) ).
cnf(t179,plain,
true = ifeq(zero,zero,less_equal(divide(sFlat0,divide(sFlat0,a)),zero),true),
inference(cp,[status(thm)],[t33,t177]) ).
cnf(t860,plain,
true = less_equal(divide(sFlat0,divide(sFlat0,a)),zero),
inference(step,[status(thm)],[t179,t11]) ).
cnf(t183,plain,
less_equal(divide(sFlat0,divide(sFlat0,a)),zero) = true,
inference(orient,[status(thm)],[t860]) ).
cnf(t184,plain,
zero = ifeq(true,true,divide(sFlat0,divide(sFlat0,a)),zero),
inference(cp,[status(thm)],[t77,t183]) ).
cnf(t861,plain,
zero = divide(sFlat0,divide(sFlat0,a)),
inference(step,[status(thm)],[t184,t11]) ).
cnf(t188,plain,
divide(sFlat0,divide(sFlat0,a)) = zero,
inference(orient,[status(thm)],[t861]) ).
cnf(t192,plain,
true = ifeq(zero,zero,less_equal(sFlat0,divide(sFlat0,a)),true),
inference(cp,[status(thm)],[t33,t188]) ).
cnf(t862,plain,
true = less_equal(sFlat0,divide(sFlat0,a)),
inference(step,[status(thm)],[t192,t11]) ).
cnf(t195,plain,
less_equal(sFlat0,divide(sFlat0,a)) = true,
inference(orient,[status(thm)],[t862]) ).
cnf(t196,plain,
divide(sFlat0,a) = ifeq(true,true,ifeq(less_equal(divide(sFlat0,a),sFlat0),true,sFlat0,divide(sFlat0,a)),divide(sFlat0,a)),
inference(cp,[status(thm)],[t12,t195]) ).
cnf(t863,plain,
divide(sFlat0,a) = ifeq(less_equal(divide(sFlat0,a),sFlat0),true,sFlat0,divide(sFlat0,a)),
inference(step,[status(thm)],[t196,t11]) ).
cnf(t864,plain,
divide(sFlat0,a) = ifeq(true,true,sFlat0,divide(sFlat0,a)),
inference(step,[status(thm)],[t863,t21]) ).
cnf(t865,plain,
divide(sFlat0,a) = sFlat0,
inference(step,[status(thm)],[t864,t11]) ).
cnf(t199,plain,
divide(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t865]) ).
cnf(t200,plain,
true = less_equal(divide(sFlat2,a),sFlat0),
inference(cp,[status(thm)],[t99,t199]) ).
cnf(t207,plain,
less_equal(divide(sFlat2,a),sFlat0) = true,
inference(orient,[status(thm)],[t200]) ).
cnf(t957,plain,
divide(sFlat2,a) = ifeq(true,true,sFlat0,divide(sFlat2,a)),
inference(step,[status(thm)],[t956,t207]) ).
cnf(t958,plain,
divide(sFlat2,a) = sFlat0,
inference(step,[status(thm)],[t957,t11]) ).
cnf(t810,plain,
divide(sFlat2,a) = sFlat0,
inference(orient,[status(thm)],[t958]) ).
cnf(t815,plain,
divide(sFlat2,a) = ifeq(less_equal(sFlat2,sFlat0),true,sFlat2,divide(sFlat2,a)),
inference(cp,[status(thm)],[t206,t810]) ).
cnf(t959,plain,
sFlat0 = ifeq(less_equal(sFlat2,sFlat0),true,sFlat2,divide(sFlat2,a)),
inference(step,[status(thm)],[t815,t810]) ).
cnf(t960,plain,
sFlat0 = ifeq(true,true,sFlat2,divide(sFlat2,a)),
inference(step,[status(thm)],[t959,t62]) ).
cnf(t961,plain,
sFlat0 = sFlat2,
inference(step,[status(thm)],[t960,t11]) ).
cnf(t825,plain,
sFlat2 = sFlat0,
inference(orient,[status(thm)],[t961]) ).
cnf(t962,plain,
divide(sFlat0,sFlat1) = sFlat0,
inference(step,[status(thm)],[t55,t825]) ).
cnf(t826,plain,
divide(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t962]) ).
cnf(f7,negated_conjecture,
divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_property_of_inversion) ).
fof(f7_nnf,plain,
divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(goal_0,negated_conjecture,
divide(divide(identity,a),divide(identity,divide(identity,a))) != divide(identity,a),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
divide(sFlat0,divide(identity,divide(identity,a))) != divide(identity,a),
inference(rw,[status(thm)],[goal_0,t16]) ).
cnf(g0_1,plain,
divide(sFlat0,divide(identity,sFlat0)) != divide(identity,a),
inference(rw,[status(thm)],[g0_0,t16]) ).
cnf(g0_2,plain,
divide(sFlat0,sFlat1) != divide(identity,a),
inference(rw,[status(thm)],[g0_1,t45]) ).
cnf(g0_3,plain,
sFlat0 != divide(identity,a),
inference(rw,[status(thm)],[g0_2,t826]) ).
cnf(g0_4,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_3,t16]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN010-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 : n014.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.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 16:16:18 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.17/1.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.17/1.56 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------