%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HEN009-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 37.04s 5.07s
% Output : Proof 37.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 97
% Number of leaves : 14
% Syntax : Number of formulae : 362 ( 338 unt; 0 def)
% Number of atoms : 410 ( 324 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 102 ( 54 ~; 48 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 1 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-4 aty)
% Number of variables : 529 ( 129 sgn 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(t253,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t259,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t253]) ).
cnf(f2,axiom,
( less_equal(Z,X)
| ~ quotient(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',divisor_existence) ).
fof(f2_nnf,plain,
! [X,Y,Z] :
( less_equal(Z,X)
| ~ quotient(X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y,Z] :
( less_equal(Z,X)
| ~ quotient(X,Y,Z) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( less_equal(X2,X0)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t228,plain,
ifeq(quotient(X1,X2,X3),true,less_equal(X3,X1),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t588,plain,
ifeq(quotient(X1,X2,X3),true,less_equal(X3,X1),true) = true,
inference(orient,[status(thm)],[t228]) ).
cnf(f7,axiom,
quotient(X,Y,divide(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure) ).
fof(f7_nnf,plain,
! [X,Y] : quotient(X,Y,divide(X,Y)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y] : quotient(X,Y,divide(X,Y)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
quotient(X0,X1,divide(X0,X1)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t57,plain,
quotient(X1,X2,divide(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t419,plain,
quotient(X1,X2,divide(X1,X2)) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(t589,plain,
true = ifeq(true,true,less_equal(divide(X1,X2),X1),true),
inference(cp,[status(thm)],[t588,t419]) ).
cnf(t56,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t56]) ).
cnf(t8406,plain,
true = less_equal(divide(X1,X2),X1),
inference(step,[status(thm)],[t589,t256]) ).
cnf(t835,plain,
less_equal(divide(X1,X2),X1) = true,
inference(orient,[status(thm)],[t8406]) ).
cnf(t840,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)],[t259,t835]) ).
cnf(t8495,plain,
divide(X1,X2) = ifeq(less_equal(X1,divide(X1,X2)),true,X1,divide(X1,X2)),
inference(step,[status(thm)],[t840,t256]) ).
cnf(t1407,plain,
ifeq(less_equal(X1,divide(X1,X2)),true,X1,divide(X1,X2)) = divide(X1,X2),
inference(orient,[status(thm)],[t8495]) ).
cnf(f1,axiom,
( less_equal(X,Y)
| ~ quotient(X,Y,zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_quotient) ).
fof(f1_nnf,plain,
! [X,Y] :
( less_equal(X,Y)
| ~ quotient(X,Y,zero) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( less_equal(X,Y)
| ~ quotient(X,Y,zero) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( less_equal(X0,X1)
| ~ quotient(X0,X1,zero) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t229,plain,
ifeq(quotient(X1,X2,zero),true,less_equal(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t735,plain,
ifeq(quotient(X1,X2,zero),true,less_equal(X1,X2),true) = true,
inference(orient,[status(thm)],[t229]) ).
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(t10,plain,
less_equal(zero,X1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t585,plain,
less_equal(zero,X1) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t586,plain,
X1 = ifeq(true,true,ifeq(less_equal(X1,zero),true,zero,X1),X1),
inference(cp,[status(thm)],[t259,t585]) ).
cnf(t8421,plain,
X1 = ifeq(less_equal(X1,zero),true,zero,X1),
inference(step,[status(thm)],[t586,t256]) ).
cnf(t1064,plain,
ifeq(less_equal(X1,zero),true,zero,X1) = X1,
inference(orient,[status(thm)],[t8421]) ).
cnf(f3,axiom,
( less_equal(V4,V5)
| ~ quotient(V1,Z,V5)
| ~ quotient(V3,V2,V4)
| ~ quotient(X,Z,V3)
| ~ quotient(Y,Z,V2)
| ~ quotient(X,Y,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
fof(f3_nnf,plain,
! [X,Y,V1,Z,V2,V3,V4,V5] :
( less_equal(V4,V5)
| ~ quotient(V1,Z,V5)
| ~ quotient(V3,V2,V4)
| ~ quotient(X,Z,V3)
| ~ quotient(Y,Z,V2)
| ~ quotient(X,Y,V1) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y,V1,Z,V2,V3,V4,V5] :
( less_equal(V4,V5)
| ~ quotient(V1,Z,V5)
| ~ quotient(V3,V2,V4)
| ~ quotient(X,Z,V3)
| ~ quotient(Y,Z,V2)
| ~ quotient(X,Y,V1) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( less_equal(X6,X7)
| ~ quotient(X2,X3,X7)
| ~ quotient(X5,X4,X6)
| ~ quotient(X0,X3,X5)
| ~ quotient(X1,X3,X4)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X1,X3,X4),true,ifeq(quotient(X0,X3,X5),true,ifeq(quotient(X5,X4,X6),true,ifeq(quotient(X2,X3,X7),true,less_equal(X6,X7),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(hi7,axiom,
quotient(X0,X1,divide(X0,X1)) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f9,hypothesis,
quotient(identity,a,idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f9_nnf,plain,
quotient(identity,a,idQa),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
quotient(identity,a,idQa),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(hi9,axiom,
quotient(identity,a,idQa) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h8,plain,
less_equal(divide(divide(V0,a),idQa),divide(divide(V0,identity),a)) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi7,hi9,hi7,hi7,hi7]) ).
cnf(f0,axiom,
( quotient(X,Y,zero)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal) ).
fof(f0_nnf,plain,
! [X,Y] :
( quotient(X,Y,zero)
| ~ less_equal(X,Y) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( quotient(X,Y,zero)
| ~ less_equal(X,Y) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(less_equal(X0,X1),true,quotient(X0,X1,zero),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h141,plain,
quotient(divide(divide(V0,a),idQa),divide(divide(V0,identity),a),zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,h8]) ).
cnf(f8,axiom,
( Z = W
| ~ quotient(X,Y,W)
| ~ quotient(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_defined) ).
fof(f8_nnf,plain,
! [X,Y,Z,W] :
( Z = W
| ~ quotient(X,Y,W)
| ~ quotient(X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y,Z,W] :
( Z = W
| ~ quotient(X,Y,W)
| ~ quotient(X,Y,Z) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( X2 = X3
| ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(quotient(X0,X1,X2),true,ifeq(quotient(X0,X1,X3),true,X2,X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t246,plain,
divide(divide(divide(X1,a),idQa),divide(divide(X1,identity),a)) = zero,
inference(hyper_resolution,[status(thm)],[hi8,hi7,h141]) ).
cnf(t260,plain,
divide(divide(divide(X1,a),idQa),divide(divide(X1,identity),a)) = zero,
inference(orient,[status(thm)],[t246]) ).
cnf(t254,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X1,X2,X4),true,X3,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t257,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X1,X2,X4),true,X3,X4),X4) = X4,
inference(orient,[status(thm)],[t254]) ).
cnf(t227,plain,
ifeq(less_equal(X1,X2),true,quotient(X1,X2,zero),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t749,plain,
ifeq(less_equal(X1,X2),true,quotient(X1,X2,zero),true) = true,
inference(orient,[status(thm)],[t227]) ).
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(t9,plain,
less_equal(X1,identity) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t533,plain,
less_equal(X1,identity) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t750,plain,
true = ifeq(true,true,quotient(X1,identity,zero),true),
inference(cp,[status(thm)],[t749,t533]) ).
cnf(t8404,plain,
true = quotient(X1,identity,zero),
inference(step,[status(thm)],[t750,t256]) ).
cnf(t809,plain,
quotient(X1,identity,zero) = true,
inference(orient,[status(thm)],[t8404]) ).
cnf(t810,plain,
X1 = ifeq(true,true,ifeq(quotient(X2,identity,X1),true,zero,X1),X1),
inference(cp,[status(thm)],[t257,t809]) ).
cnf(t8447,plain,
X1 = ifeq(quotient(X2,identity,X1),true,zero,X1),
inference(step,[status(thm)],[t810,t256]) ).
cnf(t1175,plain,
ifeq(quotient(X1,identity,X2),true,zero,X2) = X2,
inference(orient,[status(thm)],[t8447]) ).
cnf(t1176,plain,
divide(X1,identity) = ifeq(true,true,zero,divide(X1,identity)),
inference(cp,[status(thm)],[t1175,t419]) ).
cnf(t8448,plain,
divide(X1,identity) = zero,
inference(step,[status(thm)],[t1176,t256]) ).
cnf(t1177,plain,
divide(X1,identity) = zero,
inference(orient,[status(thm)],[t8448]) ).
cnf(t8449,plain,
divide(divide(divide(X1,a),idQa),divide(zero,a)) = zero,
inference(step,[status(thm)],[t260,t1177]) ).
cnf(t1065,plain,
divide(zero,X1) = ifeq(true,true,zero,divide(zero,X1)),
inference(cp,[status(thm)],[t1064,t835]) ).
cnf(t8422,plain,
divide(zero,X1) = zero,
inference(step,[status(thm)],[t1065,t256]) ).
cnf(t1067,plain,
divide(zero,X1) = zero,
inference(orient,[status(thm)],[t8422]) ).
cnf(t8450,plain,
divide(divide(divide(X1,a),idQa),zero) = zero,
inference(step,[status(thm)],[t8449,t1067]) ).
cnf(t1178,plain,
divide(divide(divide(X1,a),idQa),zero) = zero,
inference(rw,[status(thm)],[t8450]) ).
cnf(t1179,plain,
divide(divide(divide(X1,a),idQa),zero) = zero,
inference(orient,[status(thm)],[t1178]) ).
cnf(t1180,plain,
true = quotient(divide(divide(X1,a),idQa),zero,zero),
inference(cp,[status(thm)],[t419,t1179]) ).
cnf(t1283,plain,
quotient(divide(divide(X1,a),idQa),zero,zero) = true,
inference(orient,[status(thm)],[t1180]) ).
cnf(t1285,plain,
true = ifeq(true,true,less_equal(divide(divide(X1,a),idQa),zero),true),
inference(cp,[status(thm)],[t735,t1283]) ).
cnf(t8474,plain,
true = less_equal(divide(divide(X1,a),idQa),zero),
inference(step,[status(thm)],[t1285,t256]) ).
cnf(t1303,plain,
less_equal(divide(divide(X1,a),idQa),zero) = true,
inference(orient,[status(thm)],[t8474]) ).
cnf(t1304,plain,
divide(divide(X1,a),idQa) = ifeq(true,true,zero,divide(divide(X1,a),idQa)),
inference(cp,[status(thm)],[t1064,t1303]) ).
cnf(t8475,plain,
divide(divide(X1,a),idQa) = zero,
inference(step,[status(thm)],[t1304,t256]) ).
cnf(t1310,plain,
divide(divide(X1,a),idQa) = zero,
inference(orient,[status(thm)],[t8475]) ).
cnf(t1311,plain,
true = quotient(divide(X1,a),idQa,zero),
inference(cp,[status(thm)],[t419,t1310]) ).
cnf(t1312,plain,
quotient(divide(X1,a),idQa,zero) = true,
inference(orient,[status(thm)],[t1311]) ).
cnf(t1314,plain,
true = ifeq(true,true,less_equal(divide(X1,a),idQa),true),
inference(cp,[status(thm)],[t735,t1312]) ).
cnf(t8476,plain,
true = less_equal(divide(X1,a),idQa),
inference(step,[status(thm)],[t1314,t256]) ).
cnf(t1322,plain,
less_equal(divide(X1,a),idQa) = true,
inference(orient,[status(thm)],[t8476]) ).
cnf(t1325,plain,
divide(X1,a) = ifeq(less_equal(idQa,divide(X1,a)),true,ifeq(true,true,idQa,divide(X1,a)),divide(X1,a)),
inference(cp,[status(thm)],[t259,t1322]) ).
cnf(t8497,plain,
divide(X1,a) = ifeq(less_equal(idQa,divide(X1,a)),true,idQa,divide(X1,a)),
inference(step,[status(thm)],[t1325,t256]) ).
cnf(t1409,plain,
ifeq(less_equal(idQa,divide(X1,a)),true,idQa,divide(X1,a)) = divide(X1,a),
inference(orient,[status(thm)],[t8497]) ).
cnf(h7,plain,
less_equal(divide(idQa,divide(V0,a)),divide(divide(identity,V0),a)) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi7,hi7,hi9,hi7,hi7]) ).
cnf(h139,plain,
quotient(divide(idQa,divide(V0,a)),divide(divide(identity,V0),a),zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,h7]) ).
cnf(t249,plain,
divide(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a)) = zero,
inference(hyper_resolution,[status(thm)],[hi8,hi7,h139]) ).
cnf(t313,plain,
divide(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a)) = zero,
inference(orient,[status(thm)],[t249]) ).
cnf(t444,plain,
true = quotient(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a),zero),
inference(cp,[status(thm)],[t419,t313]) ).
cnf(t1410,plain,
quotient(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a),zero) = true,
inference(orient,[status(thm)],[t444]) ).
cnf(t1413,plain,
true = ifeq(true,true,less_equal(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a)),true),
inference(cp,[status(thm)],[t735,t1410]) ).
cnf(t8498,plain,
true = less_equal(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a)),
inference(step,[status(thm)],[t1413,t256]) ).
cnf(t1421,plain,
less_equal(divide(idQa,divide(X1,a)),divide(divide(identity,X1),a)) = true,
inference(orient,[status(thm)],[t8498]) ).
cnf(t468,plain,
X1 = ifeq(true,true,ifeq(quotient(X2,X3,X1),true,divide(X2,X3),X1),X1),
inference(cp,[status(thm)],[t257,t419]) ).
cnf(t8483,plain,
X1 = ifeq(quotient(X2,X3,X1),true,divide(X2,X3),X1),
inference(step,[status(thm)],[t468,t256]) ).
cnf(t1359,plain,
ifeq(quotient(X1,X2,X3),true,divide(X1,X2),X3) = X3,
inference(orient,[status(thm)],[t8483]) ).
cnf(t836,plain,
true = ifeq(true,true,quotient(divide(X1,X2),X1,zero),true),
inference(cp,[status(thm)],[t749,t835]) ).
cnf(t8417,plain,
true = quotient(divide(X1,X2),X1,zero),
inference(step,[status(thm)],[t836,t256]) ).
cnf(t982,plain,
quotient(divide(X1,X2),X1,zero) = true,
inference(orient,[status(thm)],[t8417]) ).
cnf(t1360,plain,
zero = ifeq(true,true,divide(divide(X1,X2),X1),zero),
inference(cp,[status(thm)],[t1359,t982]) ).
cnf(t8484,plain,
zero = divide(divide(X1,X2),X1),
inference(step,[status(thm)],[t1360,t256]) ).
cnf(t1376,plain,
divide(divide(X1,X2),X1) = zero,
inference(orient,[status(thm)],[t8484]) ).
cnf(t255,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X2,X4,X5),true,ifeq(quotient(X1,X4,X6),true,ifeq(quotient(X6,X5,X7),true,ifeq(quotient(X3,X4,X8),true,less_equal(X7,X8),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t606,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X2,X4,X5),true,ifeq(quotient(X1,X4,X6),true,ifeq(quotient(X6,X5,X7),true,ifeq(quotient(X3,X4,X8),true,less_equal(X7,X8),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t255]) ).
cnf(t697,plain,
true = ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X2,X4,X5),true,ifeq(quotient(X1,X4,X6),true,ifeq(quotient(X6,X5,X7),true,ifeq(true,true,less_equal(X7,divide(X3,X4)),true),true),true),true),true),
inference(cp,[status(thm)],[t606,t419]) ).
cnf(t9223,plain,
true = ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X2,X4,X5),true,ifeq(quotient(X1,X4,X6),true,ifeq(quotient(X6,X5,X7),true,less_equal(X7,divide(X3,X4)),true),true),true),true),
inference(step,[status(thm)],[t697,t256]) ).
cnf(t5726,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X2,X4,X5),true,ifeq(quotient(X1,X4,X6),true,ifeq(quotient(X6,X5,X7),true,less_equal(X7,divide(X3,X4)),true),true),true),true) = true,
inference(orient,[status(thm)],[t9223]) ).
cnf(t5729,plain,
true = ifeq(true,true,ifeq(quotient(identity,X1,X2),true,ifeq(quotient(X3,X1,X4),true,ifeq(quotient(X4,X2,X5),true,less_equal(X5,divide(zero,X1)),true),true),true),true),
inference(cp,[status(thm)],[t5726,t809]) ).
cnf(t9604,plain,
true = ifeq(quotient(identity,X1,X2),true,ifeq(quotient(X3,X1,X4),true,ifeq(quotient(X4,X2,X5),true,less_equal(X5,divide(zero,X1)),true),true),true),
inference(step,[status(thm)],[t5729,t256]) ).
cnf(t9605,plain,
true = ifeq(quotient(identity,X1,X2),true,ifeq(quotient(X3,X1,X4),true,ifeq(quotient(X4,X2,X5),true,less_equal(X5,zero),true),true),true),
inference(step,[status(thm)],[t9604,t1067]) ).
cnf(t7018,plain,
ifeq(quotient(identity,X1,X2),true,ifeq(quotient(X3,X1,X4),true,ifeq(quotient(X4,X2,X5),true,less_equal(X5,zero),true),true),true) = true,
inference(orient,[status(thm)],[t9605]) ).
cnf(t7019,plain,
true = ifeq(true,true,ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X3,divide(identity,X2),X4),true,less_equal(X4,zero),true),true),true),
inference(cp,[status(thm)],[t7018,t419]) ).
cnf(t9610,plain,
true = ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X3,divide(identity,X2),X4),true,less_equal(X4,zero),true),true),
inference(step,[status(thm)],[t7019,t256]) ).
cnf(t7030,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X3,divide(identity,X2),X4),true,less_equal(X4,zero),true),true) = true,
inference(orient,[status(thm)],[t9610]) ).
cnf(t7031,plain,
true = ifeq(true,true,ifeq(quotient(divide(X1,X2),divide(identity,X2),X3),true,less_equal(X3,zero),true),true),
inference(cp,[status(thm)],[t7030,t419]) ).
cnf(t9611,plain,
true = ifeq(quotient(divide(X1,X2),divide(identity,X2),X3),true,less_equal(X3,zero),true),
inference(step,[status(thm)],[t7031,t256]) ).
cnf(t7033,plain,
ifeq(quotient(divide(X1,X2),divide(identity,X2),X3),true,less_equal(X3,zero),true) = true,
inference(orient,[status(thm)],[t9611]) ).
cnf(t7034,plain,
true = ifeq(true,true,less_equal(divide(divide(X1,X2),divide(identity,X2)),zero),true),
inference(cp,[status(thm)],[t7033,t419]) ).
cnf(t9612,plain,
true = less_equal(divide(divide(X1,X2),divide(identity,X2)),zero),
inference(step,[status(thm)],[t7034,t256]) ).
cnf(t7035,plain,
less_equal(divide(divide(X1,X2),divide(identity,X2)),zero) = true,
inference(orient,[status(thm)],[t9612]) ).
cnf(t7036,plain,
divide(divide(X1,X2),divide(identity,X2)) = ifeq(true,true,zero,divide(divide(X1,X2),divide(identity,X2))),
inference(cp,[status(thm)],[t1064,t7035]) ).
cnf(t9613,plain,
divide(divide(X1,X2),divide(identity,X2)) = zero,
inference(step,[status(thm)],[t7036,t256]) ).
cnf(t7041,plain,
divide(divide(X1,X2),divide(identity,X2)) = zero,
inference(orient,[status(thm)],[t9613]) ).
cnf(t7044,plain,
true = quotient(divide(X1,X2),divide(identity,X2),zero),
inference(cp,[status(thm)],[t419,t7041]) ).
cnf(t7057,plain,
quotient(divide(X1,X2),divide(identity,X2),zero) = true,
inference(orient,[status(thm)],[t7044]) ).
cnf(t7059,plain,
true = ifeq(true,true,less_equal(divide(X1,X2),divide(identity,X2)),true),
inference(cp,[status(thm)],[t735,t7057]) ).
cnf(t9614,plain,
true = less_equal(divide(X1,X2),divide(identity,X2)),
inference(step,[status(thm)],[t7059,t256]) ).
cnf(t7099,plain,
less_equal(divide(X1,X2),divide(identity,X2)) = true,
inference(orient,[status(thm)],[t9614]) ).
cnf(t7103,plain,
divide(X1,X2) = ifeq(less_equal(divide(identity,X2),divide(X1,X2)),true,ifeq(true,true,divide(identity,X2),divide(X1,X2)),divide(X1,X2)),
inference(cp,[status(thm)],[t259,t7099]) ).
cnf(t9636,plain,
divide(X1,X2) = ifeq(less_equal(divide(identity,X2),divide(X1,X2)),true,divide(identity,X2),divide(X1,X2)),
inference(step,[status(thm)],[t7103,t256]) ).
cnf(t7389,plain,
ifeq(less_equal(divide(identity,X1),divide(X2,X1)),true,divide(identity,X1),divide(X2,X1)) = divide(X2,X1),
inference(orient,[status(thm)],[t9636]) ).
cnf(f10,hypothesis,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_idQa) ).
fof(f10_nnf,plain,
quotient(identity,idQa,idQ_idQa),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
quotient(identity,idQa,idQ_idQa),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(hi10,axiom,
quotient(identity,idQa,idQ_idQa) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(h13,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa)) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi9,hi7,hi10,hi7,hi7]) ).
cnf(h144,plain,
quotient(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa),zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,h13]) ).
cnf(t162,plain,
divide(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa)) = zero,
inference(hyper_resolution,[status(thm)],[hi8,hi7,h144]) ).
cnf(t342,plain,
divide(divide(idQ_idQa,divide(a,idQa)),divide(idQa,idQa)) = zero,
inference(orient,[status(thm)],[t162]) ).
cnf(hi4,axiom,
less_equal(zero,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h0,plain,
quotient(zero,V0,zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi4]) ).
cnf(hi6,axiom,
less_equal(X0,identity) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h1,plain,
quotient(V0,identity,zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi6]) ).
cnf(h121,plain,
less_equal(divide(idQa,idQa),zero) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1,hi9,hi9,hi7,h0]) ).
cnf(hi5,axiom,
ifeq(less_equal(X0,X1),true,ifeq(less_equal(X1,X0),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t2,plain,
divide(idQa,idQa) = zero,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h121]) ).
cnf(t388,plain,
divide(idQa,idQa) = zero,
inference(orient,[status(thm)],[t2]) ).
cnf(t8380,plain,
divide(divide(idQ_idQa,divide(a,idQa)),zero) = zero,
inference(step,[status(thm)],[t342,t388]) ).
cnf(t391,plain,
divide(divide(idQ_idQa,divide(a,idQa)),zero) = zero,
inference(rw,[status(thm)],[t8380]) ).
cnf(t1056,plain,
divide(divide(idQ_idQa,divide(a,idQa)),zero) = zero,
inference(orient,[status(thm)],[t391]) ).
cnf(t1057,plain,
true = quotient(divide(idQ_idQa,divide(a,idQa)),zero,zero),
inference(cp,[status(thm)],[t419,t1056]) ).
cnf(t1184,plain,
quotient(divide(idQ_idQa,divide(a,idQa)),zero,zero) = true,
inference(orient,[status(thm)],[t1057]) ).
cnf(t1186,plain,
true = ifeq(true,true,less_equal(divide(idQ_idQa,divide(a,idQa)),zero),true),
inference(cp,[status(thm)],[t735,t1184]) ).
cnf(t8454,plain,
true = less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(step,[status(thm)],[t1186,t256]) ).
cnf(t1194,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero) = true,
inference(orient,[status(thm)],[t8454]) ).
cnf(t1195,plain,
divide(idQ_idQa,divide(a,idQa)) = ifeq(true,true,zero,divide(idQ_idQa,divide(a,idQa))),
inference(cp,[status(thm)],[t1064,t1194]) ).
cnf(t8455,plain,
divide(idQ_idQa,divide(a,idQa)) = zero,
inference(step,[status(thm)],[t1195,t256]) ).
cnf(t1201,plain,
divide(idQ_idQa,divide(a,idQa)) = zero,
inference(orient,[status(thm)],[t8455]) ).
cnf(t1202,plain,
true = quotient(idQ_idQa,divide(a,idQa),zero),
inference(cp,[status(thm)],[t419,t1201]) ).
cnf(t1204,plain,
quotient(idQ_idQa,divide(a,idQa),zero) = true,
inference(orient,[status(thm)],[t1202]) ).
cnf(t1206,plain,
true = ifeq(true,true,less_equal(idQ_idQa,divide(a,idQa)),true),
inference(cp,[status(thm)],[t735,t1204]) ).
cnf(t8456,plain,
true = less_equal(idQ_idQa,divide(a,idQa)),
inference(step,[status(thm)],[t1206,t256]) ).
cnf(t1214,plain,
less_equal(idQ_idQa,divide(a,idQa)) = true,
inference(orient,[status(thm)],[t8456]) ).
cnf(t1216,plain,
divide(a,idQa) = ifeq(true,true,ifeq(less_equal(divide(a,idQa),idQ_idQa),true,idQ_idQa,divide(a,idQa)),divide(a,idQa)),
inference(cp,[status(thm)],[t259,t1214]) ).
cnf(t8496,plain,
divide(a,idQa) = ifeq(less_equal(divide(a,idQa),idQ_idQa),true,idQ_idQa,divide(a,idQa)),
inference(step,[status(thm)],[t1216,t256]) ).
cnf(t1408,plain,
ifeq(less_equal(divide(a,idQa),idQ_idQa),true,idQ_idQa,divide(a,idQa)) = divide(a,idQa),
inference(orient,[status(thm)],[t8496]) ).
cnf(t607,plain,
true = ifeq(true,true,ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X4,X2,X5),true,ifeq(quotient(X5,X3,X6),true,ifeq(quotient(divide(X4,X1),X2,X7),true,less_equal(X6,X7),true),true),true),true),true),
inference(cp,[status(thm)],[t606,t419]) ).
cnf(t8563,plain,
true = ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X4,X2,X5),true,ifeq(quotient(X5,X3,X6),true,ifeq(quotient(divide(X4,X1),X2,X7),true,less_equal(X6,X7),true),true),true),true),
inference(step,[status(thm)],[t607,t256]) ).
cnf(t1784,plain,
ifeq(quotient(X1,X2,X3),true,ifeq(quotient(X4,X2,X5),true,ifeq(quotient(X5,X3,X6),true,ifeq(quotient(divide(X4,X1),X2,X7),true,less_equal(X6,X7),true),true),true),true) = true,
inference(orient,[status(thm)],[t8563]) ).
cnf(t15,plain,
quotient(identity,idQa,idQ_idQa) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t524,plain,
quotient(identity,idQa,idQ_idQa) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t1805,plain,
true = ifeq(true,true,ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,ifeq(quotient(divide(X1,identity),idQa,X4),true,less_equal(X3,X4),true),true),true),true),
inference(cp,[status(thm)],[t1784,t524]) ).
cnf(t8671,plain,
true = ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,ifeq(quotient(divide(X1,identity),idQa,X4),true,less_equal(X3,X4),true),true),true),
inference(step,[status(thm)],[t1805,t256]) ).
cnf(t8672,plain,
true = ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,ifeq(quotient(zero,idQa,X4),true,less_equal(X3,X4),true),true),true),
inference(step,[status(thm)],[t8671,t1177]) ).
cnf(t3949,plain,
ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,ifeq(quotient(zero,idQa,X4),true,less_equal(X3,X4),true),true),true) = true,
inference(orient,[status(thm)],[t8672]) ).
cnf(t751,plain,
true = ifeq(true,true,quotient(zero,X1,zero),true),
inference(cp,[status(thm)],[t749,t585]) ).
cnf(t8405,plain,
true = quotient(zero,X1,zero),
inference(step,[status(thm)],[t751,t256]) ).
cnf(t817,plain,
quotient(zero,X1,zero) = true,
inference(orient,[status(thm)],[t8405]) ).
cnf(t3962,plain,
true = ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,ifeq(true,true,less_equal(X3,zero),true),true),true),
inference(cp,[status(thm)],[t3949,t817]) ).
cnf(t8680,plain,
true = ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,less_equal(X3,zero),true),true),
inference(step,[status(thm)],[t3962,t256]) ).
cnf(t3977,plain,
ifeq(quotient(X1,idQa,X2),true,ifeq(quotient(X2,idQ_idQa,X3),true,less_equal(X3,zero),true),true) = true,
inference(orient,[status(thm)],[t8680]) ).
cnf(t3978,plain,
true = ifeq(true,true,ifeq(quotient(divide(X1,idQa),idQ_idQa,X2),true,less_equal(X2,zero),true),true),
inference(cp,[status(thm)],[t3977,t419]) ).
cnf(t8681,plain,
true = ifeq(quotient(divide(X1,idQa),idQ_idQa,X2),true,less_equal(X2,zero),true),
inference(step,[status(thm)],[t3978,t256]) ).
cnf(t3980,plain,
ifeq(quotient(divide(X1,idQa),idQ_idQa,X2),true,less_equal(X2,zero),true) = true,
inference(orient,[status(thm)],[t8681]) ).
cnf(t3981,plain,
true = ifeq(true,true,less_equal(divide(divide(X1,idQa),idQ_idQa),zero),true),
inference(cp,[status(thm)],[t3980,t419]) ).
cnf(t8682,plain,
true = less_equal(divide(divide(X1,idQa),idQ_idQa),zero),
inference(step,[status(thm)],[t3981,t256]) ).
cnf(t3982,plain,
less_equal(divide(divide(X1,idQa),idQ_idQa),zero) = true,
inference(orient,[status(thm)],[t8682]) ).
cnf(t3983,plain,
divide(divide(X1,idQa),idQ_idQa) = ifeq(true,true,zero,divide(divide(X1,idQa),idQ_idQa)),
inference(cp,[status(thm)],[t1064,t3982]) ).
cnf(t8683,plain,
divide(divide(X1,idQa),idQ_idQa) = zero,
inference(step,[status(thm)],[t3983,t256]) ).
cnf(t3988,plain,
divide(divide(X1,idQa),idQ_idQa) = zero,
inference(orient,[status(thm)],[t8683]) ).
cnf(t3991,plain,
true = quotient(divide(X1,idQa),idQ_idQa,zero),
inference(cp,[status(thm)],[t419,t3988]) ).
cnf(t3994,plain,
quotient(divide(X1,idQa),idQ_idQa,zero) = true,
inference(orient,[status(thm)],[t3991]) ).
cnf(t3996,plain,
true = ifeq(true,true,less_equal(divide(X1,idQa),idQ_idQa),true),
inference(cp,[status(thm)],[t735,t3994]) ).
cnf(t8684,plain,
true = less_equal(divide(X1,idQa),idQ_idQa),
inference(step,[status(thm)],[t3996,t256]) ).
cnf(t4009,plain,
less_equal(divide(X1,idQa),idQ_idQa) = true,
inference(orient,[status(thm)],[t8684]) ).
cnf(t8685,plain,
ifeq(true,true,idQ_idQa,divide(a,idQa)) = divide(a,idQa),
inference(step,[status(thm)],[t1408,t4009]) ).
cnf(t8686,plain,
idQ_idQa = divide(a,idQa),
inference(step,[status(thm)],[t8685,t256]) ).
cnf(t4012,plain,
idQ_idQa = divide(a,idQa),
inference(rw,[status(thm)],[t8686]) ).
cnf(t4014,plain,
divide(a,idQa) = idQ_idQa,
inference(orient,[status(thm)],[t4012]) ).
cnf(t4018,plain,
true = quotient(idQ_idQa,a,zero),
inference(cp,[status(thm)],[t982,t4014]) ).
cnf(t4075,plain,
quotient(idQ_idQa,a,zero) = true,
inference(orient,[status(thm)],[t4018]) ).
cnf(t5747,plain,
true = ifeq(true,true,ifeq(quotient(a,X1,X2),true,ifeq(quotient(idQ_idQa,X1,X3),true,ifeq(quotient(X3,X2,X4),true,less_equal(X4,divide(zero,X1)),true),true),true),true),
inference(cp,[status(thm)],[t5726,t4075]) ).
cnf(t9660,plain,
true = ifeq(quotient(a,X1,X2),true,ifeq(quotient(idQ_idQa,X1,X3),true,ifeq(quotient(X3,X2,X4),true,less_equal(X4,divide(zero,X1)),true),true),true),
inference(step,[status(thm)],[t5747,t256]) ).
cnf(t9661,plain,
true = ifeq(quotient(a,X1,X2),true,ifeq(quotient(idQ_idQa,X1,X3),true,ifeq(quotient(X3,X2,X4),true,less_equal(X4,zero),true),true),true),
inference(step,[status(thm)],[t9660,t1067]) ).
cnf(t7550,plain,
ifeq(quotient(a,X1,X2),true,ifeq(quotient(idQ_idQa,X1,X3),true,ifeq(quotient(X3,X2,X4),true,less_equal(X4,zero),true),true),true) = true,
inference(orient,[status(thm)],[t9661]) ).
cnf(t7551,plain,
true = ifeq(true,true,ifeq(quotient(idQ_idQa,X1,X2),true,ifeq(quotient(X2,divide(a,X1),X3),true,less_equal(X3,zero),true),true),true),
inference(cp,[status(thm)],[t7550,t419]) ).
cnf(t9666,plain,
true = ifeq(quotient(idQ_idQa,X1,X2),true,ifeq(quotient(X2,divide(a,X1),X3),true,less_equal(X3,zero),true),true),
inference(step,[status(thm)],[t7551,t256]) ).
cnf(t7564,plain,
ifeq(quotient(idQ_idQa,X1,X2),true,ifeq(quotient(X2,divide(a,X1),X3),true,less_equal(X3,zero),true),true) = true,
inference(orient,[status(thm)],[t9666]) ).
cnf(f11,hypothesis,
quotient(identity,idQ_idQa,idQ__idQ_idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_idQ_idQa) ).
fof(f11_nnf,plain,
quotient(identity,idQ_idQa,idQ__idQ_idQa),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
quotient(identity,idQ_idQa,idQ__idQ_idQa),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t14,plain,
quotient(identity,idQ_idQa,idQ__idQ_idQa) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t527,plain,
quotient(identity,idQ_idQa,idQ__idQ_idQa) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(t1806,plain,
true = ifeq(true,true,ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(divide(X1,identity),idQ_idQa,X4),true,less_equal(X3,X4),true),true),true),true),
inference(cp,[status(thm)],[t1784,t527]) ).
cnf(t8740,plain,
true = ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(divide(X1,identity),idQ_idQa,X4),true,less_equal(X3,X4),true),true),true),
inference(step,[status(thm)],[t1806,t256]) ).
cnf(t8741,plain,
true = ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(zero,idQ_idQa,X4),true,less_equal(X3,X4),true),true),true),
inference(step,[status(thm)],[t8740,t1177]) ).
cnf(t4244,plain,
ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(zero,idQ_idQa,X4),true,less_equal(X3,X4),true),true),true) = true,
inference(orient,[status(thm)],[t8741]) ).
cnf(t4253,plain,
true = ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(true,true,less_equal(X3,zero),true),true),true),
inference(cp,[status(thm)],[t4244,t817]) ).
cnf(t8745,plain,
true = ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,less_equal(X3,zero),true),true),
inference(step,[status(thm)],[t4253,t256]) ).
cnf(t4260,plain,
ifeq(quotient(X1,idQ_idQa,X2),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,less_equal(X3,zero),true),true) = true,
inference(orient,[status(thm)],[t8745]) ).
cnf(t4261,plain,
true = ifeq(true,true,ifeq(quotient(divide(X1,idQ_idQa),idQ__idQ_idQa,X2),true,less_equal(X2,zero),true),true),
inference(cp,[status(thm)],[t4260,t419]) ).
cnf(t8746,plain,
true = ifeq(quotient(divide(X1,idQ_idQa),idQ__idQ_idQa,X2),true,less_equal(X2,zero),true),
inference(step,[status(thm)],[t4261,t256]) ).
cnf(t4263,plain,
ifeq(quotient(divide(X1,idQ_idQa),idQ__idQ_idQa,X2),true,less_equal(X2,zero),true) = true,
inference(orient,[status(thm)],[t8746]) ).
cnf(t4264,plain,
true = ifeq(true,true,less_equal(divide(divide(X1,idQ_idQa),idQ__idQ_idQa),zero),true),
inference(cp,[status(thm)],[t4263,t419]) ).
cnf(t8747,plain,
true = less_equal(divide(divide(X1,idQ_idQa),idQ__idQ_idQa),zero),
inference(step,[status(thm)],[t4264,t256]) ).
cnf(t4265,plain,
less_equal(divide(divide(X1,idQ_idQa),idQ__idQ_idQa),zero) = true,
inference(orient,[status(thm)],[t8747]) ).
cnf(t4266,plain,
divide(divide(X1,idQ_idQa),idQ__idQ_idQa) = ifeq(true,true,zero,divide(divide(X1,idQ_idQa),idQ__idQ_idQa)),
inference(cp,[status(thm)],[t1064,t4265]) ).
cnf(t8748,plain,
divide(divide(X1,idQ_idQa),idQ__idQ_idQa) = zero,
inference(step,[status(thm)],[t4266,t256]) ).
cnf(t4271,plain,
divide(divide(X1,idQ_idQa),idQ__idQ_idQa) = zero,
inference(orient,[status(thm)],[t8748]) ).
cnf(t4274,plain,
true = quotient(divide(X1,idQ_idQa),idQ__idQ_idQa,zero),
inference(cp,[status(thm)],[t419,t4271]) ).
cnf(t4277,plain,
quotient(divide(X1,idQ_idQa),idQ__idQ_idQa,zero) = true,
inference(orient,[status(thm)],[t4274]) ).
cnf(t4291,plain,
true = ifeq(quotient(idQ_idQa,idQ__idQ_idQa,X1),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(X3,X1,X4),true,ifeq(true,true,less_equal(X4,zero),true),true),true),true),
inference(cp,[status(thm)],[t1784,t4277]) ).
cnf(t9101,plain,
true = ifeq(quotient(idQ_idQa,idQ__idQ_idQa,X1),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(X3,X1,X4),true,less_equal(X4,zero),true),true),true),
inference(step,[status(thm)],[t4291,t256]) ).
cnf(t5356,plain,
ifeq(quotient(idQ_idQa,idQ__idQ_idQa,X1),true,ifeq(quotient(X2,idQ__idQ_idQa,X3),true,ifeq(quotient(X3,X1,X4),true,less_equal(X4,zero),true),true),true) = true,
inference(orient,[status(thm)],[t9101]) ).
cnf(t5357,plain,
true = ifeq(true,true,ifeq(quotient(X1,idQ__idQ_idQa,X2),true,ifeq(quotient(X2,divide(idQ_idQa,idQ__idQ_idQa),X3),true,less_equal(X3,zero),true),true),true),
inference(cp,[status(thm)],[t5356,t419]) ).
cnf(t9109,plain,
true = ifeq(quotient(X1,idQ__idQ_idQa,X2),true,ifeq(quotient(X2,divide(idQ_idQa,idQ__idQ_idQa),X3),true,less_equal(X3,zero),true),true),
inference(step,[status(thm)],[t5357,t256]) ).
cnf(t5374,plain,
ifeq(quotient(X1,idQ__idQ_idQa,X2),true,ifeq(quotient(X2,divide(idQ_idQa,idQ__idQ_idQa),X3),true,less_equal(X3,zero),true),true) = true,
inference(orient,[status(thm)],[t9109]) ).
cnf(t5375,plain,
true = ifeq(true,true,ifeq(quotient(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa),X2),true,less_equal(X2,zero),true),true),
inference(cp,[status(thm)],[t5374,t419]) ).
cnf(t9110,plain,
true = ifeq(quotient(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa),X2),true,less_equal(X2,zero),true),
inference(step,[status(thm)],[t5375,t256]) ).
cnf(t5377,plain,
ifeq(quotient(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa),X2),true,less_equal(X2,zero),true) = true,
inference(orient,[status(thm)],[t9110]) ).
cnf(t5378,plain,
true = ifeq(true,true,less_equal(divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)),zero),true),
inference(cp,[status(thm)],[t5377,t419]) ).
cnf(t9111,plain,
true = less_equal(divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)),zero),
inference(step,[status(thm)],[t5378,t256]) ).
cnf(t5379,plain,
less_equal(divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)),zero) = true,
inference(orient,[status(thm)],[t9111]) ).
cnf(t5380,plain,
divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)) = ifeq(true,true,zero,divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa))),
inference(cp,[status(thm)],[t1064,t5379]) ).
cnf(t9112,plain,
divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)) = zero,
inference(step,[status(thm)],[t5380,t256]) ).
cnf(t5385,plain,
divide(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)) = zero,
inference(orient,[status(thm)],[t9112]) ).
cnf(t5388,plain,
true = quotient(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa),zero),
inference(cp,[status(thm)],[t419,t5385]) ).
cnf(t5392,plain,
quotient(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa),zero) = true,
inference(orient,[status(thm)],[t5388]) ).
cnf(t5394,plain,
true = ifeq(true,true,less_equal(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)),true),
inference(cp,[status(thm)],[t735,t5392]) ).
cnf(t9113,plain,
true = less_equal(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)),
inference(step,[status(thm)],[t5394,t256]) ).
cnf(t5415,plain,
less_equal(divide(X1,idQ__idQ_idQa),divide(idQ_idQa,idQ__idQ_idQa)) = true,
inference(orient,[status(thm)],[t9113]) ).
cnf(t5417,plain,
divide(X1,idQ__idQ_idQa) = ifeq(less_equal(divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)),true,ifeq(true,true,divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)),divide(X1,idQ__idQ_idQa)),
inference(cp,[status(thm)],[t259,t5415]) ).
cnf(t9117,plain,
divide(X1,idQ__idQ_idQa) = ifeq(less_equal(divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)),true,divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)),
inference(step,[status(thm)],[t5417,t256]) ).
cnf(t5422,plain,
ifeq(less_equal(divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)),true,divide(idQ_idQa,idQ__idQ_idQa),divide(X1,idQ__idQ_idQa)) = divide(X1,idQ__idQ_idQa),
inference(orient,[status(thm)],[t9117]) ).
cnf(t7100,plain,
divide(identity,idQ__idQ_idQa) = ifeq(true,true,divide(idQ_idQa,idQ__idQ_idQa),divide(identity,idQ__idQ_idQa)),
inference(cp,[status(thm)],[t5422,t7099]) ).
cnf(t9615,plain,
divide(identity,idQ__idQ_idQa) = divide(idQ_idQa,idQ__idQ_idQa),
inference(step,[status(thm)],[t7100,t256]) ).
cnf(t7104,plain,
divide(idQ_idQa,idQ__idQ_idQa) = divide(identity,idQ__idQ_idQa),
inference(orient,[status(thm)],[t9615]) ).
cnf(t7110,plain,
true = quotient(idQ_idQa,idQ__idQ_idQa,divide(identity,idQ__idQ_idQa)),
inference(cp,[status(thm)],[t419,t7104]) ).
cnf(t7278,plain,
quotient(idQ_idQa,idQ__idQ_idQa,divide(identity,idQ__idQ_idQa)) = true,
inference(orient,[status(thm)],[t7110]) ).
cnf(t7565,plain,
true = ifeq(true,true,ifeq(quotient(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa),X1),true,less_equal(X1,zero),true),true),
inference(cp,[status(thm)],[t7564,t7278]) ).
cnf(t9667,plain,
true = ifeq(quotient(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa),X1),true,less_equal(X1,zero),true),
inference(step,[status(thm)],[t7565,t256]) ).
cnf(t7568,plain,
ifeq(quotient(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa),X1),true,less_equal(X1,zero),true) = true,
inference(orient,[status(thm)],[t9667]) ).
cnf(t7569,plain,
true = ifeq(true,true,less_equal(divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),zero),true),
inference(cp,[status(thm)],[t7568,t419]) ).
cnf(t9668,plain,
true = less_equal(divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),zero),
inference(step,[status(thm)],[t7569,t256]) ).
cnf(t7570,plain,
less_equal(divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),zero) = true,
inference(orient,[status(thm)],[t9668]) ).
cnf(t7571,plain,
divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)) = ifeq(true,true,zero,divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa))),
inference(cp,[status(thm)],[t1064,t7570]) ).
cnf(t9669,plain,
divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)) = zero,
inference(step,[status(thm)],[t7571,t256]) ).
cnf(t7576,plain,
divide(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)) = zero,
inference(orient,[status(thm)],[t9669]) ).
cnf(t7579,plain,
true = quotient(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa),zero),
inference(cp,[status(thm)],[t419,t7576]) ).
cnf(t7592,plain,
quotient(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa),zero) = true,
inference(orient,[status(thm)],[t7579]) ).
cnf(t7594,plain,
true = ifeq(true,true,less_equal(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),true),
inference(cp,[status(thm)],[t735,t7592]) ).
cnf(t9670,plain,
true = less_equal(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),
inference(step,[status(thm)],[t7594,t256]) ).
cnf(t7637,plain,
less_equal(divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)) = true,
inference(orient,[status(thm)],[t9670]) ).
cnf(t7638,plain,
divide(a,idQ__idQ_idQa) = ifeq(true,true,divide(identity,idQ__idQ_idQa),divide(a,idQ__idQ_idQa)),
inference(cp,[status(thm)],[t7389,t7637]) ).
cnf(t9671,plain,
divide(a,idQ__idQ_idQa) = divide(identity,idQ__idQ_idQa),
inference(step,[status(thm)],[t7638,t256]) ).
cnf(t7642,plain,
divide(a,idQ__idQ_idQa) = divide(identity,idQ__idQ_idQa),
inference(orient,[status(thm)],[t9671]) ).
cnf(t7644,plain,
zero = divide(divide(identity,idQ__idQ_idQa),a),
inference(cp,[status(thm)],[t1376,t7642]) ).
cnf(t7714,plain,
divide(divide(identity,idQ__idQ_idQa),a) = zero,
inference(orient,[status(thm)],[t7644]) ).
cnf(t7722,plain,
true = less_equal(divide(idQa,divide(idQ__idQ_idQa,a)),zero),
inference(cp,[status(thm)],[t1421,t7714]) ).
cnf(t7902,plain,
less_equal(divide(idQa,divide(idQ__idQ_idQa,a)),zero) = true,
inference(orient,[status(thm)],[t7722]) ).
cnf(t7903,plain,
divide(idQa,divide(idQ__idQ_idQa,a)) = ifeq(true,true,zero,divide(idQa,divide(idQ__idQ_idQa,a))),
inference(cp,[status(thm)],[t1064,t7902]) ).
cnf(t9672,plain,
divide(idQa,divide(idQ__idQ_idQa,a)) = zero,
inference(step,[status(thm)],[t7903,t256]) ).
cnf(t7908,plain,
divide(idQa,divide(idQ__idQ_idQa,a)) = zero,
inference(orient,[status(thm)],[t9672]) ).
cnf(t7911,plain,
true = quotient(idQa,divide(idQ__idQ_idQa,a),zero),
inference(cp,[status(thm)],[t419,t7908]) ).
cnf(t7950,plain,
quotient(idQa,divide(idQ__idQ_idQa,a),zero) = true,
inference(orient,[status(thm)],[t7911]) ).
cnf(t7952,plain,
true = ifeq(true,true,less_equal(idQa,divide(idQ__idQ_idQa,a)),true),
inference(cp,[status(thm)],[t735,t7950]) ).
cnf(t9673,plain,
true = less_equal(idQa,divide(idQ__idQ_idQa,a)),
inference(step,[status(thm)],[t7952,t256]) ).
cnf(t8006,plain,
less_equal(idQa,divide(idQ__idQ_idQa,a)) = true,
inference(orient,[status(thm)],[t9673]) ).
cnf(t8007,plain,
divide(idQ__idQ_idQa,a) = ifeq(true,true,idQa,divide(idQ__idQ_idQa,a)),
inference(cp,[status(thm)],[t1409,t8006]) ).
cnf(t9674,plain,
divide(idQ__idQ_idQa,a) = idQa,
inference(step,[status(thm)],[t8007,t256]) ).
cnf(t8011,plain,
divide(idQ__idQ_idQa,a) = idQa,
inference(orient,[status(thm)],[t9674]) ).
cnf(t8023,plain,
divide(idQ__idQ_idQa,a) = ifeq(less_equal(idQ__idQ_idQa,idQa),true,idQ__idQ_idQa,divide(idQ__idQ_idQa,a)),
inference(cp,[status(thm)],[t1407,t8011]) ).
cnf(t9675,plain,
idQa = ifeq(less_equal(idQ__idQ_idQa,idQa),true,idQ__idQ_idQa,divide(idQ__idQ_idQa,a)),
inference(step,[status(thm)],[t8023,t8011]) ).
cnf(hi11,axiom,
quotient(identity,idQ_idQa,idQ__idQ_idQa) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t191,plain,
less_equal(divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)),divide(idQ_idQa,idQ_idQa)) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi10,hi7,hi11,hi7,hi7]) ).
cnf(h129,plain,
less_equal(divide(idQ_idQa,divide(identity,idQa)),zero) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1,hi7,hi10,hi7,h0]) ).
cnf(t38,plain,
divide(idQ_idQa,divide(identity,idQa)) = zero,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h129]) ).
cnf(t6,plain,
divide(identity,idQa) = idQ_idQa,
inference(hyper_resolution,[status(thm)],[hi8,hi7,hi10]) ).
cnf(t409,plain,
divide(identity,idQa) = idQ_idQa,
inference(orient,[status(thm)],[t6]) ).
cnf(t8386,plain,
divide(idQ_idQa,idQ_idQa) = zero,
inference(step,[status(thm)],[t38,t409]) ).
cnf(t416,plain,
divide(idQ_idQa,idQ_idQa) = zero,
inference(orient,[status(thm)],[t8386]) ).
cnf(t8400,plain,
less_equal(divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)),zero) = true,
inference(step,[status(thm)],[t191,t416]) ).
cnf(t576,plain,
less_equal(divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)),zero) = true,
inference(orient,[status(thm)],[t8400]) ).
cnf(t1066,plain,
divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)) = ifeq(true,true,zero,divide(idQ__idQ_idQa,divide(idQa,idQ_idQa))),
inference(cp,[status(thm)],[t1064,t576]) ).
cnf(t8423,plain,
divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)) = zero,
inference(step,[status(thm)],[t1066,t256]) ).
cnf(t1068,plain,
divide(idQ__idQ_idQa,divide(idQa,idQ_idQa)) = zero,
inference(orient,[status(thm)],[t8423]) ).
cnf(t1069,plain,
true = quotient(idQ__idQ_idQa,divide(idQa,idQ_idQa),zero),
inference(cp,[status(thm)],[t419,t1068]) ).
cnf(t1070,plain,
quotient(idQ__idQ_idQa,divide(idQa,idQ_idQa),zero) = true,
inference(orient,[status(thm)],[t1069]) ).
cnf(t1072,plain,
true = ifeq(true,true,less_equal(idQ__idQ_idQa,divide(idQa,idQ_idQa)),true),
inference(cp,[status(thm)],[t735,t1070]) ).
cnf(t8424,plain,
true = less_equal(idQ__idQ_idQa,divide(idQa,idQ_idQa)),
inference(step,[status(thm)],[t1072,t256]) ).
cnf(t1080,plain,
less_equal(idQ__idQ_idQa,divide(idQa,idQ_idQa)) = true,
inference(orient,[status(thm)],[t8424]) ).
cnf(t1082,plain,
divide(idQa,idQ_idQa) = ifeq(true,true,ifeq(less_equal(divide(idQa,idQ_idQa),idQ__idQ_idQa),true,idQ__idQ_idQa,divide(idQa,idQ_idQa)),divide(idQa,idQ_idQa)),
inference(cp,[status(thm)],[t259,t1080]) ).
cnf(t8425,plain,
divide(idQa,idQ_idQa) = ifeq(less_equal(divide(idQa,idQ_idQa),idQ__idQ_idQa),true,idQ__idQ_idQa,divide(idQa,idQ_idQa)),
inference(step,[status(thm)],[t1082,t256]) ).
cnf(hi2,axiom,
ifeq(quotient(X0,X1,X2),true,less_equal(X2,X0),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h10,plain,
less_equal(idQa,identity) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi9]) ).
cnf(h71,plain,
quotient(idQa,identity,zero) = true,
inference(hyper_resolution,[status(thm)],[hi0,h10]) ).
cnf(h176,plain,
less_equal(divide(divide(idQa,idQ_idQa),idQ__idQ_idQa),zero) = true,
inference(hyper_resolution,[status(thm)],[hi3,h71,hi11,hi7,hi7,h0]) ).
cnf(t28,plain,
divide(divide(idQa,idQ_idQa),idQ__idQ_idQa) = zero,
inference(hyper_resolution,[status(thm)],[hi5,hi4,h176]) ).
cnf(t324,plain,
divide(divide(idQa,idQ_idQa),idQ__idQ_idQa) = zero,
inference(orient,[status(thm)],[t28]) ).
cnf(t439,plain,
true = quotient(divide(idQa,idQ_idQa),idQ__idQ_idQa,zero),
inference(cp,[status(thm)],[t419,t324]) ).
cnf(t927,plain,
quotient(divide(idQa,idQ_idQa),idQ__idQ_idQa,zero) = true,
inference(orient,[status(thm)],[t439]) ).
cnf(t929,plain,
true = ifeq(true,true,less_equal(divide(idQa,idQ_idQa),idQ__idQ_idQa),true),
inference(cp,[status(thm)],[t735,t927]) ).
cnf(t8411,plain,
true = less_equal(divide(idQa,idQ_idQa),idQ__idQ_idQa),
inference(step,[status(thm)],[t929,t256]) ).
cnf(t937,plain,
less_equal(divide(idQa,idQ_idQa),idQ__idQ_idQa) = true,
inference(orient,[status(thm)],[t8411]) ).
cnf(t8426,plain,
divide(idQa,idQ_idQa) = ifeq(true,true,idQ__idQ_idQa,divide(idQa,idQ_idQa)),
inference(step,[status(thm)],[t8425,t937]) ).
cnf(t8427,plain,
divide(idQa,idQ_idQa) = idQ__idQ_idQa,
inference(step,[status(thm)],[t8426,t256]) ).
cnf(t1085,plain,
divide(idQa,idQ_idQa) = idQ__idQ_idQa,
inference(orient,[status(thm)],[t8427]) ).
cnf(t1087,plain,
true = less_equal(idQ__idQ_idQa,idQa),
inference(cp,[status(thm)],[t835,t1085]) ).
cnf(t1091,plain,
less_equal(idQ__idQ_idQa,idQa) = true,
inference(orient,[status(thm)],[t1087]) ).
cnf(t9676,plain,
idQa = ifeq(true,true,idQ__idQ_idQa,divide(idQ__idQ_idQa,a)),
inference(step,[status(thm)],[t9675,t1091]) ).
cnf(t9677,plain,
idQa = idQ__idQ_idQa,
inference(step,[status(thm)],[t9676,t256]) ).
cnf(t8069,plain,
idQ__idQ_idQa = idQa,
inference(orient,[status(thm)],[t9677]) ).
cnf(f12,negated_conjecture,
idQa != idQ__idQ_idQa,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_one_inversion_equals_three) ).
fof(f12_nnf,plain,
idQa != idQ__idQ_idQa,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
idQa != idQ__idQ_idQa,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
idQa != idQ__idQ_idQa,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
idQa != idQ__idQ_idQa,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
idQa != idQa,
inference(rw,[status(thm)],[goal_0,t8069]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HEN009-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n005.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Wed Sep 23 16:15:04 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 37.04/5.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.04/5.07 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------