%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HEN011-5 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:11 PM UTC 2026
% Result : Unsatisfiable 36.67s 5.15s
% Output : Proof 36.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 20
% Syntax : Number of formulae : 276 ( 260 unt; 0 def)
% Number of atoms : 296 ( 295 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 53 ( 33 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-4 aty)
% Number of variables : 246 ( 57 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sFlat0 = divide(identity,b),
introduced(definition) ).
cnf(t120,plain,
divide(identity,b) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat1 = divide(identity,a),
introduced(definition) ).
cnf(t110,plain,
divide(identity,a) = sFlat1,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat2 = divide(identity,divide(identity,a)),
introduced(definition) ).
cnf(t86,plain,
divide(identity,divide(identity,a)) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t19313,plain,
divide(identity,sFlat1) = sFlat2,
inference(step,[status(thm)],[t86,t110]) ).
cnf(t119,plain,
divide(identity,sFlat1) = sFlat2,
inference(rw,[status(thm)],[t19313]) ).
cnf(t240,plain,
divide(identity,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t119]) ).
cnf(t17,axiom,
sFlat3 = divide(divide(identity,b),divide(identity,divide(identity,a))),
introduced(definition) ).
cnf(t68,plain,
divide(divide(identity,b),divide(identity,divide(identity,a))) = sFlat3,
inference(orient,[status(thm)],[t17]) ).
cnf(t19311,plain,
divide(divide(identity,b),sFlat2) = sFlat3,
inference(step,[status(thm)],[t68,t86]) ).
cnf(t97,plain,
divide(divide(identity,b),sFlat2) = sFlat3,
inference(rw,[status(thm)],[t19311]) ).
cnf(t19319,plain,
divide(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t97,t120]) ).
cnf(t282,plain,
divide(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t19319]) ).
cnf(t18,axiom,
sFlat4 = divide(identity,divide(identity,b)),
introduced(definition) ).
cnf(t98,plain,
divide(identity,divide(identity,b)) = sFlat4,
inference(orient,[status(thm)],[t18]) ).
cnf(t19314,plain,
divide(identity,sFlat0) = sFlat4,
inference(step,[status(thm)],[t98,t120]) ).
cnf(t129,plain,
divide(identity,sFlat0) = sFlat4,
inference(rw,[status(thm)],[t19314]) ).
cnf(t260,plain,
divide(identity,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t129]) ).
cnf(t19,axiom,
sFlat5 = divide(divide(identity,a),divide(identity,divide(identity,b))),
introduced(definition) ).
cnf(t60,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) = sFlat5,
inference(orient,[status(thm)],[t19]) ).
cnf(t19312,plain,
divide(divide(identity,a),sFlat4) = sFlat5,
inference(step,[status(thm)],[t60,t98]) ).
cnf(t109,plain,
divide(divide(identity,a),sFlat4) = sFlat5,
inference(rw,[status(thm)],[t19312]) ).
cnf(t19320,plain,
divide(sFlat1,sFlat4) = sFlat5,
inference(step,[status(thm)],[t109,t110]) ).
cnf(t316,plain,
divide(sFlat1,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t19320]) ).
cnf(f3,axiom,
( X = Y
| divide(Y,X) != zero
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',divide_and_equal) ).
fof(f3_nnf,plain,
! [X,Y] :
( X = Y
| divide(Y,X) != zero
| divide(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] :
( X = Y
| divide(Y,X) != zero
| divide(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( X0 = X1
| divide(X1,X0) != zero
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t11,plain,
ifeq(divide(X1,X2),zero,ifeq(divide(X2,X1),zero,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t22,plain,
ifeq(divide(X1,X2),zero,ifeq(divide(X2,X1),zero,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(f8,axiom,
( divide(divide(X,Z),Y) = zero
| divide(divide(X,Y),Z) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide1) ).
fof(f8_nnf,plain,
! [X,Y,Z] :
( divide(divide(X,Z),Y) = zero
| divide(divide(X,Y),Z) != zero ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y,Z] :
( divide(divide(X,Z),Y) = zero
| divide(divide(X,Y),Z) != zero ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( divide(divide(X0,X2),X1) = zero
| divide(divide(X0,X1),X2) != zero ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t12,plain,
ifeq(divide(divide(X1,X2),X3),zero,divide(divide(X1,X3),X2),zero) = zero,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t218,plain,
ifeq(divide(divide(X1,X2),X3),zero,divide(divide(X1,X3),X2),zero) = zero,
inference(orient,[status(thm)],[t12]) ).
cnf(f1,axiom,
divide(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
fof(f1_nnf,plain,
! [X,Z,Y] : divide(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)) = zero,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Z,Y] : divide(divide(divide(X,Z),divide(Y,Z)),divide(divide(X,Y),Z)) = zero,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = zero,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t8,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t36,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t53,plain,
zero = divide(divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)),divide(zero,Y3)),
inference(cp,[status(thm)],[t36,t36]) ).
cnf(f2,axiom,
divide(zero,X) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_is_smallest) ).
fof(f2_nnf,plain,
! [X] : divide(zero,X) = zero,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : divide(zero,X) = zero,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
divide(zero,X0) = zero,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
divide(zero,X1) = zero,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t76,plain,
divide(zero,X1) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t20040,plain,
zero = divide(divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)),zero),
inference(step,[status(thm)],[t53,t76]) ).
cnf(f6,axiom,
divide(X,zero) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_zero_is_x) ).
fof(f6_nnf,plain,
! [X] : divide(X,zero) = X,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] : divide(X,zero) = X,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
divide(X0,zero) = X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t2,plain,
divide(X1,zero) = X1,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t20,plain,
divide(X1,zero) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t20041,plain,
zero = divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)),
inference(step,[status(thm)],[t20040,t20]) ).
cnf(t16537,plain,
divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)) = zero,
inference(orient,[status(thm)],[t20041]) ).
cnf(t48,plain,
divide(divide(X1,X2),X3) = ifeq(zero,zero,ifeq(divide(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),zero,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)),divide(divide(X1,X2),X3)),
inference(cp,[status(thm)],[t22,t36]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t19705,plain,
divide(divide(X1,X2),X3) = ifeq(divide(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),zero,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)),
inference(step,[status(thm)],[t48,t21]) ).
cnf(t4381,plain,
ifeq(divide(divide(divide(X1,X2),X3),divide(divide(X1,X3),divide(X2,X3))),zero,divide(divide(X1,X3),divide(X2,X3)),divide(divide(X1,X2),X3)) = divide(divide(X1,X2),X3),
inference(orient,[status(thm)],[t19705]) ).
cnf(f5,axiom,
divide(X,X) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
fof(f5_nnf,plain,
! [X] : divide(X,X) = zero,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] : divide(X,X) = zero,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
divide(X0,X0) = zero,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
divide(X1,X1) = zero,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t25,plain,
divide(X1,X1) = zero,
inference(orient,[status(thm)],[t0]) ).
cnf(t221,plain,
zero = ifeq(zero,zero,divide(divide(X1,divide(X1,X2)),X2),zero),
inference(cp,[status(thm)],[t218,t25]) ).
cnf(t19400,plain,
zero = divide(divide(X1,divide(X1,X2)),X2),
inference(step,[status(thm)],[t221,t21]) ).
cnf(t738,plain,
divide(divide(X1,divide(X1,X2)),X2) = zero,
inference(orient,[status(thm)],[t19400]) ).
cnf(t739,plain,
zero = divide(divide(sFlat1,sFlat5),sFlat4),
inference(cp,[status(thm)],[t738,t316]) ).
cnf(t753,plain,
divide(divide(sFlat1,sFlat5),sFlat4) = zero,
inference(orient,[status(thm)],[t739]) ).
cnf(t4810,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = ifeq(divide(divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4),divide(divide(X1,sFlat4),zero)),zero,divide(divide(X1,sFlat4),divide(divide(sFlat1,sFlat5),sFlat4)),divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4)),
inference(cp,[status(thm)],[t4381,t753]) ).
cnf(t19799,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = ifeq(divide(divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4),divide(X1,sFlat4)),zero,divide(divide(X1,sFlat4),divide(divide(sFlat1,sFlat5),sFlat4)),divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4)),
inference(step,[status(thm)],[t4810,t20]) ).
cnf(f10,axiom,
( divide(divide(X,Z),divide(Y,Z)) = zero
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide3) ).
fof(f10_nnf,plain,
! [X,Y,Z] :
( divide(divide(X,Z),divide(Y,Z)) = zero
| divide(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y,Z] :
( divide(divide(X,Z),divide(Y,Z)) = zero
| divide(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( divide(divide(X0,X2),divide(X1,X2)) = zero
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t9,plain,
ifeq(divide(X1,X2),zero,divide(divide(X1,X3),divide(X2,X3)),zero) = zero,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t158,plain,
ifeq(divide(X1,X2),zero,divide(divide(X1,X3),divide(X2,X3)),zero) = zero,
inference(orient,[status(thm)],[t9]) ).
cnf(f0,axiom,
divide(divide(X,Y),X) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_smaller_than_numerator) ).
fof(f0_nnf,plain,
! [X,Y] : divide(divide(X,Y),X) = zero,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : divide(divide(X,Y),X) = zero,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
divide(divide(X0,X1),X0) = zero,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,plain,
divide(divide(X1,X2),X1) = zero,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t29,plain,
divide(divide(X1,X2),X1) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t165,plain,
zero = ifeq(zero,zero,divide(divide(divide(X1,X2),X3),divide(X1,X3)),zero),
inference(cp,[status(thm)],[t158,t29]) ).
cnf(t19681,plain,
zero = divide(divide(divide(X1,X2),X3),divide(X1,X3)),
inference(step,[status(thm)],[t165,t21]) ).
cnf(t3878,plain,
divide(divide(divide(X1,X2),X3),divide(X1,X3)) = zero,
inference(orient,[status(thm)],[t19681]) ).
cnf(t19800,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = ifeq(zero,zero,divide(divide(X1,sFlat4),divide(divide(sFlat1,sFlat5),sFlat4)),divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4)),
inference(step,[status(thm)],[t19799,t3878]) ).
cnf(t19801,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = divide(divide(X1,sFlat4),divide(divide(sFlat1,sFlat5),sFlat4)),
inference(step,[status(thm)],[t19800,t21]) ).
cnf(t19802,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = divide(divide(X1,sFlat4),zero),
inference(step,[status(thm)],[t19801,t753]) ).
cnf(t19803,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = divide(X1,sFlat4),
inference(step,[status(thm)],[t19802,t20]) ).
cnf(t6587,plain,
divide(divide(X1,divide(sFlat1,sFlat5)),sFlat4) = divide(X1,sFlat4),
inference(orient,[status(thm)],[t19803]) ).
cnf(f11,axiom,
divide(identity,divide(identity,divide(identity,X))) = divide(identity,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_inversion_equals_three) ).
fof(f11_nnf,plain,
! [X] : divide(identity,divide(identity,divide(identity,X))) = divide(identity,X),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : divide(identity,divide(identity,divide(identity,X))) = divide(identity,X),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
divide(identity,divide(identity,divide(identity,X0))) = divide(identity,X0),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t6,plain,
divide(identity,divide(identity,divide(identity,X1))) = divide(identity,X1),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t79,plain,
divide(identity,divide(identity,divide(identity,X1))) = divide(identity,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t113,plain,
divide(identity,a) = divide(identity,divide(identity,sFlat1)),
inference(cp,[status(thm)],[t79,t110]) ).
cnf(t19325,plain,
sFlat1 = divide(identity,divide(identity,sFlat1)),
inference(step,[status(thm)],[t113,t110]) ).
cnf(t19326,plain,
sFlat1 = divide(identity,sFlat2),
inference(step,[status(thm)],[t19325,t240]) ).
cnf(t352,plain,
divide(identity,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t19326]) ).
cnf(t362,plain,
zero = ifeq(divide(X1,identity),zero,divide(divide(X1,sFlat2),sFlat1),zero),
inference(cp,[status(thm)],[t158,t352]) ).
cnf(f4,axiom,
divide(X,identity) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
fof(f4_nnf,plain,
! [X] : divide(X,identity) = zero,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : divide(X,identity) = zero,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
divide(X0,identity) = zero,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t1,plain,
divide(X1,identity) = zero,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t26,plain,
divide(X1,identity) = zero,
inference(orient,[status(thm)],[t1]) ).
cnf(t19374,plain,
zero = ifeq(zero,zero,divide(divide(X1,sFlat2),sFlat1),zero),
inference(step,[status(thm)],[t362,t26]) ).
cnf(t19375,plain,
zero = divide(divide(X1,sFlat2),sFlat1),
inference(step,[status(thm)],[t19374,t21]) ).
cnf(t550,plain,
divide(divide(X1,sFlat2),sFlat1) = zero,
inference(orient,[status(thm)],[t19375]) ).
cnf(t557,plain,
zero = ifeq(zero,zero,divide(divide(divide(X1,sFlat2),X2),divide(sFlat1,X2)),zero),
inference(cp,[status(thm)],[t158,t550]) ).
cnf(t19995,plain,
zero = divide(divide(divide(X1,sFlat2),X2),divide(sFlat1,X2)),
inference(step,[status(thm)],[t557,t21]) ).
cnf(t14440,plain,
divide(divide(divide(X1,sFlat2),X2),divide(sFlat1,X2)) = zero,
inference(orient,[status(thm)],[t19995]) ).
cnf(t14452,plain,
divide(divide(divide(X1,sFlat2),sFlat5),sFlat4) = divide(zero,sFlat4),
inference(cp,[status(thm)],[t6587,t14440]) ).
cnf(t19997,plain,
divide(divide(divide(X1,sFlat2),sFlat5),sFlat4) = zero,
inference(step,[status(thm)],[t14452,t76]) ).
cnf(t14560,plain,
divide(divide(divide(X1,sFlat2),sFlat5),sFlat4) = zero,
inference(orient,[status(thm)],[t19997]) ).
cnf(t17005,plain,
zero = divide(divide(divide(divide(X1,sFlat5),divide(sFlat2,sFlat5)),sFlat4),zero),
inference(cp,[status(thm)],[t16537,t14560]) ).
cnf(t20054,plain,
zero = divide(divide(divide(X1,sFlat5),divide(sFlat2,sFlat5)),sFlat4),
inference(step,[status(thm)],[t17005,t20]) ).
cnf(f9,axiom,
( divide(divide(Z,Y),divide(Z,X)) = zero
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide2) ).
fof(f9_nnf,plain,
! [X,Y,Z] :
( divide(divide(Z,Y),divide(Z,X)) = zero
| divide(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X,Y,Z] :
( divide(divide(Z,Y),divide(Z,X)) = zero
| divide(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( divide(divide(X2,X1),divide(X2,X0)) = zero
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t10,plain,
ifeq(divide(X1,X2),zero,divide(divide(X3,X2),divide(X3,X1)),zero) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t130,plain,
ifeq(divide(X1,X2),zero,divide(divide(X3,X2),divide(X3,X1)),zero) = zero,
inference(orient,[status(thm)],[t10]) ).
cnf(t317,plain,
zero = divide(sFlat5,sFlat1),
inference(cp,[status(thm)],[t29,t316]) ).
cnf(t334,plain,
divide(sFlat5,sFlat1) = zero,
inference(orient,[status(thm)],[t317]) ).
cnf(t345,plain,
zero = ifeq(zero,zero,divide(divide(X1,sFlat1),divide(X1,sFlat5)),zero),
inference(cp,[status(thm)],[t130,t334]) ).
cnf(t19427,plain,
zero = divide(divide(X1,sFlat1),divide(X1,sFlat5)),
inference(step,[status(thm)],[t345,t21]) ).
cnf(t934,plain,
divide(divide(X1,sFlat1),divide(X1,sFlat5)) = zero,
inference(orient,[status(thm)],[t19427]) ).
cnf(f12,axiom,
divide(divide(identity,X),divide(identity,divide(identity,X))) = divide(identity,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_inversion) ).
fof(f12_nnf,plain,
! [X] : divide(divide(identity,X),divide(identity,divide(identity,X))) = divide(identity,X),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] : divide(divide(identity,X),divide(identity,divide(identity,X))) = divide(identity,X),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
divide(divide(identity,X0),divide(identity,divide(identity,X0))) = divide(identity,X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t7,plain,
divide(divide(identity,X1),divide(identity,divide(identity,X1))) = divide(identity,X1),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t54,plain,
divide(divide(identity,X1),divide(identity,divide(identity,X1))) = divide(identity,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t255,plain,
divide(identity,sFlat1) = divide(sFlat2,divide(identity,divide(identity,sFlat1))),
inference(cp,[status(thm)],[t54,t240]) ).
cnf(t19353,plain,
sFlat2 = divide(sFlat2,divide(identity,divide(identity,sFlat1))),
inference(step,[status(thm)],[t255,t240]) ).
cnf(t19354,plain,
sFlat2 = divide(sFlat2,divide(identity,sFlat2)),
inference(step,[status(thm)],[t19353,t240]) ).
cnf(t19355,plain,
sFlat2 = divide(sFlat2,sFlat1),
inference(step,[status(thm)],[t19354,t352]) ).
cnf(t479,plain,
divide(sFlat2,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t19355]) ).
cnf(t935,plain,
zero = divide(sFlat2,divide(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t934,t479]) ).
cnf(t952,plain,
divide(sFlat2,divide(sFlat2,sFlat5)) = zero,
inference(orient,[status(thm)],[t935]) ).
cnf(t953,plain,
divide(sFlat2,sFlat5) = ifeq(zero,zero,ifeq(divide(divide(sFlat2,sFlat5),sFlat2),zero,sFlat2,divide(sFlat2,sFlat5)),divide(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t22,t952]) ).
cnf(t19428,plain,
divide(sFlat2,sFlat5) = ifeq(divide(divide(sFlat2,sFlat5),sFlat2),zero,sFlat2,divide(sFlat2,sFlat5)),
inference(step,[status(thm)],[t953,t21]) ).
cnf(t19429,plain,
divide(sFlat2,sFlat5) = ifeq(zero,zero,sFlat2,divide(sFlat2,sFlat5)),
inference(step,[status(thm)],[t19428,t29]) ).
cnf(t19430,plain,
divide(sFlat2,sFlat5) = sFlat2,
inference(step,[status(thm)],[t19429,t21]) ).
cnf(t964,plain,
divide(sFlat2,sFlat5) = sFlat2,
inference(orient,[status(thm)],[t19430]) ).
cnf(t20055,plain,
zero = divide(divide(divide(X1,sFlat5),sFlat2),sFlat4),
inference(step,[status(thm)],[t20054,t964]) ).
cnf(t17920,plain,
divide(divide(divide(X1,sFlat5),sFlat2),sFlat4) = zero,
inference(orient,[status(thm)],[t20055]) ).
cnf(t17928,plain,
zero = ifeq(zero,zero,divide(divide(divide(X1,sFlat5),sFlat4),sFlat2),zero),
inference(cp,[status(thm)],[t218,t17920]) ).
cnf(t20067,plain,
zero = divide(divide(divide(X1,sFlat5),sFlat4),sFlat2),
inference(step,[status(thm)],[t17928,t21]) ).
cnf(t18242,plain,
divide(divide(divide(X1,sFlat5),sFlat4),sFlat2) = zero,
inference(orient,[status(thm)],[t20067]) ).
cnf(t18270,plain,
zero = divide(divide(divide(divide(X1,sFlat4),divide(sFlat5,sFlat4)),sFlat2),zero),
inference(cp,[status(thm)],[t16537,t18242]) ).
cnf(t20095,plain,
zero = divide(divide(divide(X1,sFlat4),divide(sFlat5,sFlat4)),sFlat2),
inference(step,[status(thm)],[t18270,t20]) ).
cnf(t764,plain,
zero = divide(divide(divide(sFlat1,sFlat4),divide(sFlat5,sFlat4)),zero),
inference(cp,[status(thm)],[t36,t753]) ).
cnf(t19401,plain,
zero = divide(divide(sFlat1,sFlat4),divide(sFlat5,sFlat4)),
inference(step,[status(thm)],[t764,t20]) ).
cnf(t19402,plain,
zero = divide(sFlat5,divide(sFlat5,sFlat4)),
inference(step,[status(thm)],[t19401,t316]) ).
cnf(t779,plain,
divide(sFlat5,divide(sFlat5,sFlat4)) = zero,
inference(orient,[status(thm)],[t19402]) ).
cnf(t780,plain,
divide(sFlat5,sFlat4) = ifeq(zero,zero,ifeq(divide(divide(sFlat5,sFlat4),sFlat5),zero,sFlat5,divide(sFlat5,sFlat4)),divide(sFlat5,sFlat4)),
inference(cp,[status(thm)],[t22,t779]) ).
cnf(t19403,plain,
divide(sFlat5,sFlat4) = ifeq(divide(divide(sFlat5,sFlat4),sFlat5),zero,sFlat5,divide(sFlat5,sFlat4)),
inference(step,[status(thm)],[t780,t21]) ).
cnf(t19404,plain,
divide(sFlat5,sFlat4) = ifeq(zero,zero,sFlat5,divide(sFlat5,sFlat4)),
inference(step,[status(thm)],[t19403,t29]) ).
cnf(t19405,plain,
divide(sFlat5,sFlat4) = sFlat5,
inference(step,[status(thm)],[t19404,t21]) ).
cnf(t791,plain,
divide(sFlat5,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t19405]) ).
cnf(t20096,plain,
zero = divide(divide(divide(X1,sFlat4),sFlat5),sFlat2),
inference(step,[status(thm)],[t20095,t791]) ).
cnf(t19138,plain,
divide(divide(divide(X1,sFlat4),sFlat5),sFlat2) = zero,
inference(orient,[status(thm)],[t20096]) ).
cnf(t123,plain,
divide(identity,b) = divide(identity,divide(identity,sFlat0)),
inference(cp,[status(thm)],[t79,t120]) ).
cnf(t19337,plain,
sFlat0 = divide(identity,divide(identity,sFlat0)),
inference(step,[status(thm)],[t123,t120]) ).
cnf(t19338,plain,
sFlat0 = divide(identity,sFlat4),
inference(step,[status(thm)],[t19337,t260]) ).
cnf(t408,plain,
divide(identity,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t19338]) ).
cnf(t422,plain,
divide(identity,sFlat4) = divide(sFlat0,divide(identity,divide(identity,sFlat4))),
inference(cp,[status(thm)],[t54,t408]) ).
cnf(t19339,plain,
sFlat0 = divide(sFlat0,divide(identity,divide(identity,sFlat4))),
inference(step,[status(thm)],[t422,t408]) ).
cnf(t19340,plain,
sFlat0 = divide(sFlat0,divide(identity,sFlat0)),
inference(step,[status(thm)],[t19339,t408]) ).
cnf(t19341,plain,
sFlat0 = divide(sFlat0,sFlat4),
inference(step,[status(thm)],[t19340,t260]) ).
cnf(t427,plain,
divide(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t19341]) ).
cnf(t19139,plain,
zero = divide(divide(sFlat0,sFlat5),sFlat2),
inference(cp,[status(thm)],[t19138,t427]) ).
cnf(t19188,plain,
divide(divide(sFlat0,sFlat5),sFlat2) = zero,
inference(orient,[status(thm)],[t19139]) ).
cnf(t19199,plain,
zero = ifeq(zero,zero,divide(divide(sFlat0,sFlat2),sFlat5),zero),
inference(cp,[status(thm)],[t218,t19188]) ).
cnf(t20097,plain,
zero = divide(divide(sFlat0,sFlat2),sFlat5),
inference(step,[status(thm)],[t19199,t21]) ).
cnf(t20098,plain,
zero = divide(sFlat3,sFlat5),
inference(step,[status(thm)],[t20097,t282]) ).
cnf(t19236,plain,
divide(sFlat3,sFlat5) = zero,
inference(orient,[status(thm)],[t20098]) ).
cnf(t19237,plain,
sFlat5 = ifeq(zero,zero,ifeq(divide(sFlat5,sFlat3),zero,sFlat3,sFlat5),sFlat5),
inference(cp,[status(thm)],[t22,t19236]) ).
cnf(t20099,plain,
sFlat5 = ifeq(divide(sFlat5,sFlat3),zero,sFlat3,sFlat5),
inference(step,[status(thm)],[t19237,t21]) ).
cnf(t740,plain,
zero = divide(divide(sFlat0,sFlat3),sFlat2),
inference(cp,[status(thm)],[t738,t282]) ).
cnf(t766,plain,
divide(divide(sFlat0,sFlat3),sFlat2) = zero,
inference(orient,[status(thm)],[t740]) ).
cnf(t4807,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = ifeq(divide(divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2),divide(divide(X1,sFlat2),zero)),zero,divide(divide(X1,sFlat2),divide(divide(sFlat0,sFlat3),sFlat2)),divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2)),
inference(cp,[status(thm)],[t4381,t766]) ).
cnf(t19789,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = ifeq(divide(divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2),divide(X1,sFlat2)),zero,divide(divide(X1,sFlat2),divide(divide(sFlat0,sFlat3),sFlat2)),divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2)),
inference(step,[status(thm)],[t4807,t20]) ).
cnf(t19790,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = ifeq(zero,zero,divide(divide(X1,sFlat2),divide(divide(sFlat0,sFlat3),sFlat2)),divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2)),
inference(step,[status(thm)],[t19789,t3878]) ).
cnf(t19791,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = divide(divide(X1,sFlat2),divide(divide(sFlat0,sFlat3),sFlat2)),
inference(step,[status(thm)],[t19790,t21]) ).
cnf(t19792,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = divide(divide(X1,sFlat2),zero),
inference(step,[status(thm)],[t19791,t766]) ).
cnf(t19793,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = divide(X1,sFlat2),
inference(step,[status(thm)],[t19792,t20]) ).
cnf(t6488,plain,
divide(divide(X1,divide(sFlat0,sFlat3)),sFlat2) = divide(X1,sFlat2),
inference(orient,[status(thm)],[t19793]) ).
cnf(t418,plain,
zero = ifeq(divide(X1,identity),zero,divide(divide(X1,sFlat4),sFlat0),zero),
inference(cp,[status(thm)],[t158,t408]) ).
cnf(t19381,plain,
zero = ifeq(zero,zero,divide(divide(X1,sFlat4),sFlat0),zero),
inference(step,[status(thm)],[t418,t26]) ).
cnf(t19382,plain,
zero = divide(divide(X1,sFlat4),sFlat0),
inference(step,[status(thm)],[t19381,t21]) ).
cnf(t604,plain,
divide(divide(X1,sFlat4),sFlat0) = zero,
inference(orient,[status(thm)],[t19382]) ).
cnf(t611,plain,
zero = ifeq(zero,zero,divide(divide(divide(X1,sFlat4),X2),divide(sFlat0,X2)),zero),
inference(cp,[status(thm)],[t158,t604]) ).
cnf(t20009,plain,
zero = divide(divide(divide(X1,sFlat4),X2),divide(sFlat0,X2)),
inference(step,[status(thm)],[t611,t21]) ).
cnf(t14938,plain,
divide(divide(divide(X1,sFlat4),X2),divide(sFlat0,X2)) = zero,
inference(orient,[status(thm)],[t20009]) ).
cnf(t14948,plain,
divide(divide(divide(X1,sFlat4),sFlat3),sFlat2) = divide(zero,sFlat2),
inference(cp,[status(thm)],[t6488,t14938]) ).
cnf(t20011,plain,
divide(divide(divide(X1,sFlat4),sFlat3),sFlat2) = zero,
inference(step,[status(thm)],[t14948,t76]) ).
cnf(t15056,plain,
divide(divide(divide(X1,sFlat4),sFlat3),sFlat2) = zero,
inference(orient,[status(thm)],[t20011]) ).
cnf(t16999,plain,
zero = divide(divide(divide(divide(X1,sFlat3),divide(sFlat4,sFlat3)),sFlat2),zero),
inference(cp,[status(thm)],[t16537,t15056]) ).
cnf(t20050,plain,
zero = divide(divide(divide(X1,sFlat3),divide(sFlat4,sFlat3)),sFlat2),
inference(step,[status(thm)],[t16999,t20]) ).
cnf(t283,plain,
zero = divide(sFlat3,sFlat0),
inference(cp,[status(thm)],[t29,t282]) ).
cnf(t300,plain,
divide(sFlat3,sFlat0) = zero,
inference(orient,[status(thm)],[t283]) ).
cnf(t311,plain,
zero = ifeq(zero,zero,divide(divide(X1,sFlat0),divide(X1,sFlat3)),zero),
inference(cp,[status(thm)],[t130,t300]) ).
cnf(t19420,plain,
zero = divide(divide(X1,sFlat0),divide(X1,sFlat3)),
inference(step,[status(thm)],[t311,t21]) ).
cnf(t861,plain,
divide(divide(X1,sFlat0),divide(X1,sFlat3)) = zero,
inference(orient,[status(thm)],[t19420]) ).
cnf(t275,plain,
divide(identity,sFlat0) = divide(sFlat4,divide(identity,divide(identity,sFlat0))),
inference(cp,[status(thm)],[t54,t260]) ).
cnf(t19362,plain,
sFlat4 = divide(sFlat4,divide(identity,divide(identity,sFlat0))),
inference(step,[status(thm)],[t275,t260]) ).
cnf(t19363,plain,
sFlat4 = divide(sFlat4,divide(identity,sFlat4)),
inference(step,[status(thm)],[t19362,t260]) ).
cnf(t19364,plain,
sFlat4 = divide(sFlat4,sFlat0),
inference(step,[status(thm)],[t19363,t408]) ).
cnf(t508,plain,
divide(sFlat4,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t19364]) ).
cnf(t862,plain,
zero = divide(sFlat4,divide(sFlat4,sFlat3)),
inference(cp,[status(thm)],[t861,t508]) ).
cnf(t879,plain,
divide(sFlat4,divide(sFlat4,sFlat3)) = zero,
inference(orient,[status(thm)],[t862]) ).
cnf(t880,plain,
divide(sFlat4,sFlat3) = ifeq(zero,zero,ifeq(divide(divide(sFlat4,sFlat3),sFlat4),zero,sFlat4,divide(sFlat4,sFlat3)),divide(sFlat4,sFlat3)),
inference(cp,[status(thm)],[t22,t879]) ).
cnf(t19421,plain,
divide(sFlat4,sFlat3) = ifeq(divide(divide(sFlat4,sFlat3),sFlat4),zero,sFlat4,divide(sFlat4,sFlat3)),
inference(step,[status(thm)],[t880,t21]) ).
cnf(t19422,plain,
divide(sFlat4,sFlat3) = ifeq(zero,zero,sFlat4,divide(sFlat4,sFlat3)),
inference(step,[status(thm)],[t19421,t29]) ).
cnf(t19423,plain,
divide(sFlat4,sFlat3) = sFlat4,
inference(step,[status(thm)],[t19422,t21]) ).
cnf(t891,plain,
divide(sFlat4,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t19423]) ).
cnf(t20051,plain,
zero = divide(divide(divide(X1,sFlat3),sFlat4),sFlat2),
inference(step,[status(thm)],[t20050,t891]) ).
cnf(t17831,plain,
divide(divide(divide(X1,sFlat3),sFlat4),sFlat2) = zero,
inference(orient,[status(thm)],[t20051]) ).
cnf(t17839,plain,
zero = ifeq(zero,zero,divide(divide(divide(X1,sFlat3),sFlat2),sFlat4),zero),
inference(cp,[status(thm)],[t218,t17831]) ).
cnf(t20063,plain,
zero = divide(divide(divide(X1,sFlat3),sFlat2),sFlat4),
inference(step,[status(thm)],[t17839,t21]) ).
cnf(t18098,plain,
divide(divide(divide(X1,sFlat3),sFlat2),sFlat4) = zero,
inference(orient,[status(thm)],[t20063]) ).
cnf(t18126,plain,
zero = divide(divide(divide(divide(X1,sFlat2),divide(sFlat3,sFlat2)),sFlat4),zero),
inference(cp,[status(thm)],[t16537,t18098]) ).
cnf(t20071,plain,
zero = divide(divide(divide(X1,sFlat2),divide(sFlat3,sFlat2)),sFlat4),
inference(step,[status(thm)],[t18126,t20]) ).
cnf(t777,plain,
zero = divide(divide(divide(sFlat0,sFlat2),divide(sFlat3,sFlat2)),zero),
inference(cp,[status(thm)],[t36,t766]) ).
cnf(t19406,plain,
zero = divide(divide(sFlat0,sFlat2),divide(sFlat3,sFlat2)),
inference(step,[status(thm)],[t777,t20]) ).
cnf(t19407,plain,
zero = divide(sFlat3,divide(sFlat3,sFlat2)),
inference(step,[status(thm)],[t19406,t282]) ).
cnf(t805,plain,
divide(sFlat3,divide(sFlat3,sFlat2)) = zero,
inference(orient,[status(thm)],[t19407]) ).
cnf(t806,plain,
divide(sFlat3,sFlat2) = ifeq(zero,zero,ifeq(divide(divide(sFlat3,sFlat2),sFlat3),zero,sFlat3,divide(sFlat3,sFlat2)),divide(sFlat3,sFlat2)),
inference(cp,[status(thm)],[t22,t805]) ).
cnf(t19408,plain,
divide(sFlat3,sFlat2) = ifeq(divide(divide(sFlat3,sFlat2),sFlat3),zero,sFlat3,divide(sFlat3,sFlat2)),
inference(step,[status(thm)],[t806,t21]) ).
cnf(t19409,plain,
divide(sFlat3,sFlat2) = ifeq(zero,zero,sFlat3,divide(sFlat3,sFlat2)),
inference(step,[status(thm)],[t19408,t29]) ).
cnf(t19410,plain,
divide(sFlat3,sFlat2) = sFlat3,
inference(step,[status(thm)],[t19409,t21]) ).
cnf(t817,plain,
divide(sFlat3,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t19410]) ).
cnf(t20072,plain,
zero = divide(divide(divide(X1,sFlat2),sFlat3),sFlat4),
inference(step,[status(thm)],[t20071,t817]) ).
cnf(t18418,plain,
divide(divide(divide(X1,sFlat2),sFlat3),sFlat4) = zero,
inference(orient,[status(thm)],[t20072]) ).
cnf(t366,plain,
divide(identity,sFlat2) = divide(sFlat1,divide(identity,divide(identity,sFlat2))),
inference(cp,[status(thm)],[t54,t352]) ).
cnf(t19327,plain,
sFlat1 = divide(sFlat1,divide(identity,divide(identity,sFlat2))),
inference(step,[status(thm)],[t366,t352]) ).
cnf(t19328,plain,
sFlat1 = divide(sFlat1,divide(identity,sFlat1)),
inference(step,[status(thm)],[t19327,t352]) ).
cnf(t19329,plain,
sFlat1 = divide(sFlat1,sFlat2),
inference(step,[status(thm)],[t19328,t240]) ).
cnf(t371,plain,
divide(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t19329]) ).
cnf(t18419,plain,
zero = divide(divide(sFlat1,sFlat3),sFlat4),
inference(cp,[status(thm)],[t18418,t371]) ).
cnf(t18468,plain,
divide(divide(sFlat1,sFlat3),sFlat4) = zero,
inference(orient,[status(thm)],[t18419]) ).
cnf(t18479,plain,
zero = ifeq(zero,zero,divide(divide(sFlat1,sFlat4),sFlat3),zero),
inference(cp,[status(thm)],[t218,t18468]) ).
cnf(t20073,plain,
zero = divide(divide(sFlat1,sFlat4),sFlat3),
inference(step,[status(thm)],[t18479,t21]) ).
cnf(t20074,plain,
zero = divide(sFlat5,sFlat3),
inference(step,[status(thm)],[t20073,t316]) ).
cnf(t18516,plain,
divide(sFlat5,sFlat3) = zero,
inference(orient,[status(thm)],[t20074]) ).
cnf(t20100,plain,
sFlat5 = ifeq(zero,zero,sFlat3,sFlat5),
inference(step,[status(thm)],[t20099,t18516]) ).
cnf(t20101,plain,
sFlat5 = sFlat3,
inference(step,[status(thm)],[t20100,t21]) ).
cnf(t19267,plain,
sFlat5 = sFlat3,
inference(orient,[status(thm)],[t20101]) ).
cnf(t20102,plain,
divide(sFlat1,sFlat4) = sFlat3,
inference(step,[status(thm)],[t316,t19267]) ).
cnf(t19268,plain,
divide(sFlat1,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t20102]) ).
cnf(f13,negated_conjecture,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f13_nnf,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
divide(divide(identity,b),divide(identity,divide(identity,a))) != divide(divide(identity,a),divide(identity,divide(identity,b))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
divide(sFlat0,divide(identity,divide(identity,a))) != divide(divide(identity,a),divide(identity,divide(identity,b))),
inference(rw,[status(thm)],[goal_0,t120]) ).
cnf(g0_1,plain,
divide(sFlat0,divide(identity,sFlat1)) != divide(divide(identity,a),divide(identity,divide(identity,b))),
inference(rw,[status(thm)],[g0_0,t110]) ).
cnf(g0_2,plain,
divide(sFlat0,sFlat2) != divide(divide(identity,a),divide(identity,divide(identity,b))),
inference(rw,[status(thm)],[g0_1,t240]) ).
cnf(g0_3,plain,
sFlat3 != divide(divide(identity,a),divide(identity,divide(identity,b))),
inference(rw,[status(thm)],[g0_2,t282]) ).
cnf(g0_4,plain,
sFlat3 != divide(sFlat1,divide(identity,divide(identity,b))),
inference(rw,[status(thm)],[g0_3,t110]) ).
cnf(g0_5,plain,
sFlat3 != divide(sFlat1,divide(identity,sFlat0)),
inference(rw,[status(thm)],[g0_4,t120]) ).
cnf(g0_6,plain,
sFlat3 != divide(sFlat1,sFlat4),
inference(rw,[status(thm)],[g0_5,t260]) ).
cnf(g0_7,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_6,t19268]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HEN011-5 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.44 % Computer : n002.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Wed Sep 23 16:20:34 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 36.67/5.15 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.67/5.15 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------