%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HEN011-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 : n012.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 8.02s 6.49s
% Output : Proof 8.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 14
% Syntax : Number of formulae : 391 ( 379 unt; 0 def)
% Number of atoms : 407 ( 374 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 42 ( 26 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-4 aty)
% Number of variables : 349 ( 147 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,hypothesis,
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',part_of_theorem) ).
fof(f7_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)],[f7]) ).
fof(f7_sk,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
divide(divide(identity,a),divide(identity,divide(identity,b))) != divide(divide(identity,b),divide(identity,divide(identity,a))),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t17,plain,
ifeq(divide(divide(identity,a),divide(identity,divide(identity,b))),divide(divide(identity,b),divide(identity,divide(identity,a))),false,true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f8,hypothesis,
divide(identity,a) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f8_nnf,plain,
divide(identity,a) = c,
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
divide(identity,a) = c,
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t1,plain,
divide(identity,a) = c,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t48,plain,
divide(identity,a) = c,
inference(orient,[status(thm)],[t1]) ).
cnf(t5695,plain,
ifeq(divide(c,divide(identity,divide(identity,b))),divide(divide(identity,b),divide(identity,divide(identity,a))),false,true) = true,
inference(step,[status(thm)],[t17,t48]) ).
cnf(f9,hypothesis,
divide(identity,b) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_b) ).
fof(f9_nnf,plain,
divide(identity,b) = d,
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
divide(identity,b) = d,
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t2,plain,
divide(identity,b) = d,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t44,plain,
divide(identity,b) = d,
inference(orient,[status(thm)],[t2]) ).
cnf(t5696,plain,
ifeq(divide(c,divide(identity,d)),divide(divide(identity,b),divide(identity,divide(identity,a))),false,true) = true,
inference(step,[status(thm)],[t5695,t44]) ).
cnf(f11,hypothesis,
divide(identity,d) = g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_d) ).
fof(f11_nnf,plain,
divide(identity,d) = g,
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
divide(identity,d) = g,
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t4,plain,
divide(identity,d) = g,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t40,plain,
divide(identity,d) = g,
inference(orient,[status(thm)],[t4]) ).
cnf(t5697,plain,
ifeq(divide(c,g),divide(divide(identity,b),divide(identity,divide(identity,a))),false,true) = true,
inference(step,[status(thm)],[t5696,t40]) ).
cnf(t5698,plain,
ifeq(divide(c,g),divide(d,divide(identity,divide(identity,a))),false,true) = true,
inference(step,[status(thm)],[t5697,t44]) ).
cnf(t5699,plain,
ifeq(divide(c,g),divide(d,divide(identity,c)),false,true) = true,
inference(step,[status(thm)],[t5698,t48]) ).
cnf(f10,hypothesis,
divide(identity,c) = e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_c) ).
fof(f10_nnf,plain,
divide(identity,c) = e,
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
divide(identity,c) = e,
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t3,plain,
divide(identity,c) = e,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t36,plain,
divide(identity,c) = e,
inference(orient,[status(thm)],[t3]) ).
cnf(t5700,plain,
ifeq(divide(c,g),divide(d,e),false,true) = true,
inference(step,[status(thm)],[t5699,t36]) ).
cnf(t102,plain,
ifeq(divide(c,g),divide(d,e),false,true) = true,
inference(orient,[status(thm)],[t5700]) ).
cnf(f5,axiom,
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_and_equal) ).
fof(f5_nnf,plain,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( X = Y
| ~ less_equal(Y,X)
| ~ less_equal(X,Y) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( X0 = X1
| ~ less_equal(X1,X0)
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t15,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t19,plain,
ifeq(less_equal(X1,X2),true,ifeq(less_equal(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(f1,axiom,
( less_equal(X,Y)
| divide(X,Y) != zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal2) ).
fof(f1_nnf,plain,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( less_equal(X,Y)
| divide(X,Y) != zero ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( less_equal(X0,X1)
| divide(X0,X1) != zero ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t11,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t97,plain,
ifeq(divide(X1,X2),zero,less_equal(X1,X2),true) = true,
inference(orient,[status(thm)],[t11]) ).
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(t16,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t64,plain,
less_equal(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(f0,axiom,
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal1) ).
fof(f0_nnf,plain,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( divide(X,Y) = zero
| ~ less_equal(X,Y) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( divide(X0,X1) = zero
| ~ less_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(less_equal(X0,X1),true,divide(X0,X1),zero) = zero,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(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(hi2,axiom,
less_equal(divide(X0,X1),X0) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t8,plain,
divide(divide(X1,X2),X1) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi2]) ).
cnf(t21,plain,
divide(divide(X1,X2),X1) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t80,plain,
true = less_equal(divide(divide(X1,X2),zero),divide(divide(X1,divide(X2,X3)),X2)),
inference(cp,[status(thm)],[t64,t21]) ).
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(t7,plain,
less_equal(zero,X1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t94,plain,
less_equal(zero,X1) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t96,plain,
zero = ifeq(less_equal(X1,zero),true,ifeq(true,true,X1,zero),zero),
inference(cp,[status(thm)],[t19,t94]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t5744,plain,
zero = ifeq(less_equal(X1,zero),true,X1,zero),
inference(step,[status(thm)],[t96,t18]) ).
cnf(t235,plain,
ifeq(less_equal(X1,zero),true,X1,zero) = zero,
inference(orient,[status(thm)],[t5744]) ).
cnf(hi3,axiom,
less_equal(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t14,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi3]) ).
cnf(t24,plain,
divide(divide(divide(X1,X2),divide(X3,X2)),divide(divide(X1,X3),X2)) = zero,
inference(orient,[status(thm)],[t14]) ).
cnf(hi4,axiom,
less_equal(zero,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t5,plain,
divide(zero,X1) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi4]) ).
cnf(t52,plain,
divide(zero,X1) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t53,plain,
zero = divide(divide(divide(X1,X2),zero),divide(divide(X1,zero),X2)),
inference(cp,[status(thm)],[t24,t52]) ).
cnf(t1472,plain,
divide(divide(divide(X1,X2),zero),divide(divide(X1,zero),X2)) = zero,
inference(orient,[status(thm)],[t53]) ).
cnf(t27,plain,
zero = divide(divide(divide(X1,X2),zero),divide(divide(X1,divide(X2,X3)),X2)),
inference(cp,[status(thm)],[t24,t21]) ).
cnf(t242,plain,
divide(divide(divide(X1,X2),zero),divide(divide(X1,divide(X2,X3)),X2)) = zero,
inference(orient,[status(thm)],[t27]) ).
cnf(t247,plain,
zero = divide(divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t242,t21]) ).
cnf(t274,plain,
divide(divide(divide(X1,X1),zero),zero) = zero,
inference(orient,[status(thm)],[t247]) ).
cnf(t276,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,X1),zero),zero),true),
inference(cp,[status(thm)],[t97,t274]) ).
cnf(t5745,plain,
true = less_equal(divide(divide(X1,X1),zero),zero),
inference(step,[status(thm)],[t276,t18]) ).
cnf(t282,plain,
less_equal(divide(divide(X1,X1),zero),zero) = true,
inference(orient,[status(thm)],[t5745]) ).
cnf(t283,plain,
zero = ifeq(true,true,divide(divide(X1,X1),zero),zero),
inference(cp,[status(thm)],[t235,t282]) ).
cnf(t5746,plain,
zero = divide(divide(X1,X1),zero),
inference(step,[status(thm)],[t283,t18]) ).
cnf(t287,plain,
divide(divide(X1,X1),zero) = zero,
inference(orient,[status(thm)],[t5746]) ).
cnf(t289,plain,
true = ifeq(zero,zero,less_equal(divide(X1,X1),zero),true),
inference(cp,[status(thm)],[t97,t287]) ).
cnf(t5747,plain,
true = less_equal(divide(X1,X1),zero),
inference(step,[status(thm)],[t289,t18]) ).
cnf(t296,plain,
less_equal(divide(X1,X1),zero) = true,
inference(orient,[status(thm)],[t5747]) ).
cnf(t297,plain,
zero = ifeq(true,true,divide(X1,X1),zero),
inference(cp,[status(thm)],[t235,t296]) ).
cnf(t5748,plain,
zero = divide(X1,X1),
inference(step,[status(thm)],[t297,t18]) ).
cnf(t301,plain,
divide(X1,X1) = zero,
inference(orient,[status(thm)],[t5748]) ).
cnf(t1490,plain,
zero = divide(divide(divide(X1,divide(X1,zero)),zero),zero),
inference(cp,[status(thm)],[t1472,t301]) ).
cnf(t1640,plain,
divide(divide(divide(X1,divide(X1,zero)),zero),zero) = zero,
inference(orient,[status(thm)],[t1490]) ).
cnf(t1642,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,divide(X1,zero)),zero),zero),true),
inference(cp,[status(thm)],[t97,t1640]) ).
cnf(t5874,plain,
true = less_equal(divide(divide(X1,divide(X1,zero)),zero),zero),
inference(step,[status(thm)],[t1642,t18]) ).
cnf(t2194,plain,
less_equal(divide(divide(X1,divide(X1,zero)),zero),zero) = true,
inference(orient,[status(thm)],[t5874]) ).
cnf(t2195,plain,
zero = ifeq(true,true,divide(divide(X1,divide(X1,zero)),zero),zero),
inference(cp,[status(thm)],[t235,t2194]) ).
cnf(t5875,plain,
zero = divide(divide(X1,divide(X1,zero)),zero),
inference(step,[status(thm)],[t2195,t18]) ).
cnf(t2199,plain,
divide(divide(X1,divide(X1,zero)),zero) = zero,
inference(orient,[status(thm)],[t5875]) ).
cnf(t2201,plain,
true = ifeq(zero,zero,less_equal(divide(X1,divide(X1,zero)),zero),true),
inference(cp,[status(thm)],[t97,t2199]) ).
cnf(t5876,plain,
true = less_equal(divide(X1,divide(X1,zero)),zero),
inference(step,[status(thm)],[t2201,t18]) ).
cnf(t2217,plain,
less_equal(divide(X1,divide(X1,zero)),zero) = true,
inference(orient,[status(thm)],[t5876]) ).
cnf(t2218,plain,
zero = ifeq(true,true,divide(X1,divide(X1,zero)),zero),
inference(cp,[status(thm)],[t235,t2217]) ).
cnf(t5877,plain,
zero = divide(X1,divide(X1,zero)),
inference(step,[status(thm)],[t2218,t18]) ).
cnf(t2222,plain,
divide(X1,divide(X1,zero)) = zero,
inference(orient,[status(thm)],[t5877]) ).
cnf(t2224,plain,
true = ifeq(zero,zero,less_equal(X1,divide(X1,zero)),true),
inference(cp,[status(thm)],[t97,t2222]) ).
cnf(t5878,plain,
true = less_equal(X1,divide(X1,zero)),
inference(step,[status(thm)],[t2224,t18]) ).
cnf(t2251,plain,
less_equal(X1,divide(X1,zero)) = true,
inference(orient,[status(thm)],[t5878]) ).
cnf(t2254,plain,
divide(X1,zero) = ifeq(true,true,ifeq(less_equal(divide(X1,zero),X1),true,X1,divide(X1,zero)),divide(X1,zero)),
inference(cp,[status(thm)],[t19,t2251]) ).
cnf(t5879,plain,
divide(X1,zero) = ifeq(less_equal(divide(X1,zero),X1),true,X1,divide(X1,zero)),
inference(step,[status(thm)],[t2254,t18]) ).
cnf(t10,plain,
less_equal(divide(X1,X2),X1) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t57,plain,
less_equal(divide(X1,X2),X1) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t5880,plain,
divide(X1,zero) = ifeq(true,true,X1,divide(X1,zero)),
inference(step,[status(thm)],[t5879,t57]) ).
cnf(t5881,plain,
divide(X1,zero) = X1,
inference(step,[status(thm)],[t5880,t18]) ).
cnf(t2256,plain,
divide(X1,zero) = X1,
inference(orient,[status(thm)],[t5881]) ).
cnf(t6119,plain,
true = less_equal(divide(X1,X2),divide(divide(X1,divide(X2,X3)),X2)),
inference(step,[status(thm)],[t80,t2256]) ).
cnf(t4845,plain,
less_equal(divide(X1,X2),divide(divide(X1,divide(X2,X3)),X2)) = true,
inference(orient,[status(thm)],[t6119]) ).
cnf(t4912,plain,
divide(divide(X1,divide(X2,X3)),X2) = ifeq(true,true,ifeq(less_equal(divide(divide(X1,divide(X2,X3)),X2),divide(X1,X2)),true,divide(X1,X2),divide(divide(X1,divide(X2,X3)),X2)),divide(divide(X1,divide(X2,X3)),X2)),
inference(cp,[status(thm)],[t19,t4845]) ).
cnf(t6120,plain,
divide(divide(X1,divide(X2,X3)),X2) = ifeq(less_equal(divide(divide(X1,divide(X2,X3)),X2),divide(X1,X2)),true,divide(X1,X2),divide(divide(X1,divide(X2,X3)),X2)),
inference(step,[status(thm)],[t4912,t18]) ).
cnf(t30,plain,
zero = divide(divide(divide(divide(X1,X2),X3),divide(X1,X3)),divide(zero,X3)),
inference(cp,[status(thm)],[t24,t21]) ).
cnf(t5782,plain,
zero = divide(divide(divide(divide(X1,X2),X3),divide(X1,X3)),zero),
inference(step,[status(thm)],[t30,t52]) ).
cnf(t557,plain,
divide(divide(divide(divide(X1,X2),X3),divide(X1,X3)),zero) = zero,
inference(orient,[status(thm)],[t5782]) ).
cnf(t5887,plain,
divide(divide(divide(X1,X2),X3),divide(X1,X3)) = zero,
inference(step,[status(thm)],[t557,t2256]) ).
cnf(t2263,plain,
divide(divide(divide(X1,X2),X3),divide(X1,X3)) = zero,
inference(rw,[status(thm)],[t5887]) ).
cnf(t2512,plain,
divide(divide(divide(X1,X2),X3),divide(X1,X3)) = zero,
inference(orient,[status(thm)],[t2263]) ).
cnf(t2544,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,X2),X3),divide(X1,X3)),true),
inference(cp,[status(thm)],[t97,t2512]) ).
cnf(t5931,plain,
true = less_equal(divide(divide(X1,X2),X3),divide(X1,X3)),
inference(step,[status(thm)],[t2544,t18]) ).
cnf(t2825,plain,
less_equal(divide(divide(X1,X2),X3),divide(X1,X3)) = true,
inference(orient,[status(thm)],[t5931]) ).
cnf(t6121,plain,
divide(divide(X1,divide(X2,X3)),X2) = ifeq(true,true,divide(X1,X2),divide(divide(X1,divide(X2,X3)),X2)),
inference(step,[status(thm)],[t6120,t2825]) ).
cnf(t6122,plain,
divide(divide(X1,divide(X2,X3)),X2) = divide(X1,X2),
inference(step,[status(thm)],[t6121,t18]) ).
cnf(t4914,plain,
divide(divide(X1,divide(X2,X3)),X2) = divide(X1,X2),
inference(orient,[status(thm)],[t6122]) ).
cnf(t35,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)],[t24,t24]) ).
cnf(t5908,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)],[t35,t52]) ).
cnf(t5909,plain,
zero = divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)),
inference(step,[status(thm)],[t5908,t2256]) ).
cnf(t2377,plain,
divide(divide(divide(divide(X1,X2),divide(X3,X2)),Y3),divide(divide(divide(X1,X3),X2),Y3)) = zero,
inference(orient,[status(thm)],[t5909]) ).
cnf(t79,plain,
true = less_equal(divide(divide(X1,d),g),divide(divide(X1,identity),d)),
inference(cp,[status(thm)],[t64,t40]) ).
cnf(f6,axiom,
less_equal(X,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
fof(f6_nnf,plain,
! [X] : less_equal(X,identity),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] : less_equal(X,identity),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
less_equal(X0,identity),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
less_equal(X0,identity) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t0,plain,
divide(X1,identity) = zero,
inference(hyper_resolution,[status(thm)],[hi0,hi6]) ).
cnf(t20,plain,
divide(X1,identity) = zero,
inference(orient,[status(thm)],[t0]) ).
cnf(t5733,plain,
true = less_equal(divide(divide(X1,d),g),divide(zero,d)),
inference(step,[status(thm)],[t79,t20]) ).
cnf(t5734,plain,
true = less_equal(divide(divide(X1,d),g),zero),
inference(step,[status(thm)],[t5733,t52]) ).
cnf(t203,plain,
less_equal(divide(divide(X1,d),g),zero) = true,
inference(orient,[status(thm)],[t5734]) ).
cnf(t207,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,d),g)),true,divide(divide(X1,d),g),zero),zero),
inference(cp,[status(thm)],[t19,t203]) ).
cnf(t5739,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,d),g)),true,divide(divide(X1,d),g),zero),
inference(step,[status(thm)],[t207,t18]) ).
cnf(t5740,plain,
zero = ifeq(true,true,divide(divide(X1,d),g),zero),
inference(step,[status(thm)],[t5739,t94]) ).
cnf(t5741,plain,
zero = divide(divide(X1,d),g),
inference(step,[status(thm)],[t5740,t18]) ).
cnf(t222,plain,
divide(divide(X1,d),g) = zero,
inference(orient,[status(thm)],[t5741]) ).
cnf(t2536,plain,
zero = divide(divide(divide(divide(X1,d),X2),g),zero),
inference(cp,[status(thm)],[t2512,t222]) ).
cnf(t5914,plain,
zero = divide(divide(divide(X1,d),X2),g),
inference(step,[status(thm)],[t2536,t2256]) ).
cnf(t2601,plain,
divide(divide(divide(X1,d),X2),g) = zero,
inference(orient,[status(thm)],[t5914]) ).
cnf(t2610,plain,
zero = divide(divide(divide(divide(X1,X2),divide(d,X2)),g),zero),
inference(cp,[status(thm)],[t2377,t2601]) ).
cnf(t5946,plain,
zero = divide(divide(divide(X1,X2),divide(d,X2)),g),
inference(step,[status(thm)],[t2610,t2256]) ).
cnf(t3081,plain,
divide(divide(divide(X1,X2),divide(d,X2)),g) = zero,
inference(orient,[status(thm)],[t5946]) ).
cnf(t78,plain,
true = less_equal(divide(divide(X1,c),e),divide(divide(X1,identity),c)),
inference(cp,[status(thm)],[t64,t36]) ).
cnf(t5723,plain,
true = less_equal(divide(divide(X1,c),e),divide(zero,c)),
inference(step,[status(thm)],[t78,t20]) ).
cnf(t5724,plain,
true = less_equal(divide(divide(X1,c),e),zero),
inference(step,[status(thm)],[t5723,t52]) ).
cnf(t172,plain,
less_equal(divide(divide(X1,c),e),zero) = true,
inference(orient,[status(thm)],[t5724]) ).
cnf(t176,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,c),e)),true,divide(divide(X1,c),e),zero),zero),
inference(cp,[status(thm)],[t19,t172]) ).
cnf(t5729,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,c),e)),true,divide(divide(X1,c),e),zero),
inference(step,[status(thm)],[t176,t18]) ).
cnf(t5730,plain,
zero = ifeq(true,true,divide(divide(X1,c),e),zero),
inference(step,[status(thm)],[t5729,t94]) ).
cnf(t5731,plain,
zero = divide(divide(X1,c),e),
inference(step,[status(thm)],[t5730,t18]) ).
cnf(t191,plain,
divide(divide(X1,c),e) = zero,
inference(orient,[status(thm)],[t5731]) ).
cnf(t195,plain,
true = less_equal(divide(divide(X1,e),divide(c,e)),zero),
inference(cp,[status(thm)],[t64,t191]) ).
cnf(t436,plain,
less_equal(divide(divide(X1,e),divide(c,e)),zero) = true,
inference(orient,[status(thm)],[t195]) ).
cnf(t437,plain,
zero = ifeq(true,true,divide(divide(X1,e),divide(c,e)),zero),
inference(cp,[status(thm)],[t235,t436]) ).
cnf(t5767,plain,
zero = divide(divide(X1,e),divide(c,e)),
inference(step,[status(thm)],[t437,t18]) ).
cnf(t443,plain,
divide(divide(X1,e),divide(c,e)) = zero,
inference(orient,[status(thm)],[t5767]) ).
cnf(t445,plain,
true = ifeq(zero,zero,less_equal(divide(X1,e),divide(c,e)),true),
inference(cp,[status(thm)],[t97,t443]) ).
cnf(t5768,plain,
true = less_equal(divide(X1,e),divide(c,e)),
inference(step,[status(thm)],[t445,t18]) ).
cnf(t454,plain,
less_equal(divide(X1,e),divide(c,e)) = true,
inference(orient,[status(thm)],[t5768]) ).
cnf(t49,plain,
zero = divide(divide(c,divide(X1,a)),divide(divide(identity,X1),a)),
inference(cp,[status(thm)],[t24,t48]) ).
cnf(t1391,plain,
divide(divide(c,divide(X1,a)),divide(divide(identity,X1),a)) = zero,
inference(orient,[status(thm)],[t49]) ).
cnf(t76,plain,
true = less_equal(divide(divide(X1,a),c),divide(divide(X1,identity),a)),
inference(cp,[status(thm)],[t64,t48]) ).
cnf(t5703,plain,
true = less_equal(divide(divide(X1,a),c),divide(zero,a)),
inference(step,[status(thm)],[t76,t20]) ).
cnf(t5704,plain,
true = less_equal(divide(divide(X1,a),c),zero),
inference(step,[status(thm)],[t5703,t52]) ).
cnf(t110,plain,
less_equal(divide(divide(X1,a),c),zero) = true,
inference(orient,[status(thm)],[t5704]) ).
cnf(t114,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,a),c)),true,divide(divide(X1,a),c),zero),zero),
inference(cp,[status(thm)],[t19,t110]) ).
cnf(t5709,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,a),c)),true,divide(divide(X1,a),c),zero),
inference(step,[status(thm)],[t114,t18]) ).
cnf(t5710,plain,
zero = ifeq(true,true,divide(divide(X1,a),c),zero),
inference(step,[status(thm)],[t5709,t94]) ).
cnf(t5711,plain,
zero = divide(divide(X1,a),c),
inference(step,[status(thm)],[t5710,t18]) ).
cnf(t129,plain,
divide(divide(X1,a),c) = zero,
inference(orient,[status(thm)],[t5711]) ).
cnf(t133,plain,
true = less_equal(divide(divide(X1,c),divide(a,c)),zero),
inference(cp,[status(thm)],[t64,t129]) ).
cnf(t330,plain,
less_equal(divide(divide(X1,c),divide(a,c)),zero) = true,
inference(orient,[status(thm)],[t133]) ).
cnf(t331,plain,
true = less_equal(divide(e,divide(a,c)),zero),
inference(cp,[status(thm)],[t330,t36]) ).
cnf(t338,plain,
less_equal(divide(e,divide(a,c)),zero) = true,
inference(orient,[status(thm)],[t331]) ).
cnf(t339,plain,
zero = ifeq(true,true,divide(e,divide(a,c)),zero),
inference(cp,[status(thm)],[t235,t338]) ).
cnf(t5753,plain,
zero = divide(e,divide(a,c)),
inference(step,[status(thm)],[t339,t18]) ).
cnf(t345,plain,
divide(e,divide(a,c)) = zero,
inference(orient,[status(thm)],[t5753]) ).
cnf(t347,plain,
true = ifeq(zero,zero,less_equal(e,divide(a,c)),true),
inference(cp,[status(thm)],[t97,t345]) ).
cnf(t5754,plain,
true = less_equal(e,divide(a,c)),
inference(step,[status(thm)],[t347,t18]) ).
cnf(t354,plain,
less_equal(e,divide(a,c)) = true,
inference(orient,[status(thm)],[t5754]) ).
cnf(t355,plain,
divide(a,c) = ifeq(true,true,ifeq(less_equal(divide(a,c),e),true,e,divide(a,c)),divide(a,c)),
inference(cp,[status(thm)],[t19,t354]) ).
cnf(t5755,plain,
divide(a,c) = ifeq(less_equal(divide(a,c),e),true,e,divide(a,c)),
inference(step,[status(thm)],[t355,t18]) ).
cnf(t193,plain,
true = ifeq(zero,zero,less_equal(divide(X1,c),e),true),
inference(cp,[status(thm)],[t97,t191]) ).
cnf(t5732,plain,
true = less_equal(divide(X1,c),e),
inference(step,[status(thm)],[t193,t18]) ).
cnf(t200,plain,
less_equal(divide(X1,c),e) = true,
inference(orient,[status(thm)],[t5732]) ).
cnf(t5756,plain,
divide(a,c) = ifeq(true,true,e,divide(a,c)),
inference(step,[status(thm)],[t5755,t200]) ).
cnf(t5757,plain,
divide(a,c) = e,
inference(step,[status(thm)],[t5756,t18]) ).
cnf(t357,plain,
divide(a,c) = e,
inference(orient,[status(thm)],[t5757]) ).
cnf(t358,plain,
zero = divide(e,a),
inference(cp,[status(thm)],[t21,t357]) ).
cnf(t368,plain,
divide(e,a) = zero,
inference(orient,[status(thm)],[t358]) ).
cnf(t1393,plain,
zero = divide(divide(c,zero),divide(divide(identity,e),a)),
inference(cp,[status(thm)],[t1391,t368]) ).
cnf(t1413,plain,
divide(divide(c,zero),divide(divide(identity,e),a)) = zero,
inference(orient,[status(thm)],[t1393]) ).
cnf(t1415,plain,
true = ifeq(zero,zero,less_equal(divide(c,zero),divide(divide(identity,e),a)),true),
inference(cp,[status(thm)],[t97,t1413]) ).
cnf(t5838,plain,
true = less_equal(divide(c,zero),divide(divide(identity,e),a)),
inference(step,[status(thm)],[t1415,t18]) ).
cnf(t1448,plain,
less_equal(divide(c,zero),divide(divide(identity,e),a)) = true,
inference(orient,[status(thm)],[t5838]) ).
cnf(t5882,plain,
less_equal(c,divide(divide(identity,e),a)) = true,
inference(step,[status(thm)],[t1448,t2256]) ).
cnf(t2258,plain,
less_equal(c,divide(divide(identity,e),a)) = true,
inference(rw,[status(thm)],[t5882]) ).
cnf(t2267,plain,
less_equal(c,divide(divide(identity,e),a)) = true,
inference(orient,[status(thm)],[t2258]) ).
cnf(t2270,plain,
divide(divide(identity,e),a) = ifeq(true,true,ifeq(less_equal(divide(divide(identity,e),a),c),true,c,divide(divide(identity,e),a)),divide(divide(identity,e),a)),
inference(cp,[status(thm)],[t19,t2267]) ).
cnf(t5890,plain,
divide(divide(identity,e),a) = ifeq(less_equal(divide(divide(identity,e),a),c),true,c,divide(divide(identity,e),a)),
inference(step,[status(thm)],[t2270,t18]) ).
cnf(t131,plain,
true = ifeq(zero,zero,less_equal(divide(X1,a),c),true),
inference(cp,[status(thm)],[t97,t129]) ).
cnf(t5712,plain,
true = less_equal(divide(X1,a),c),
inference(step,[status(thm)],[t131,t18]) ).
cnf(t138,plain,
less_equal(divide(X1,a),c) = true,
inference(orient,[status(thm)],[t5712]) ).
cnf(t5891,plain,
divide(divide(identity,e),a) = ifeq(true,true,c,divide(divide(identity,e),a)),
inference(step,[status(thm)],[t5890,t138]) ).
cnf(t5892,plain,
divide(divide(identity,e),a) = c,
inference(step,[status(thm)],[t5891,t18]) ).
cnf(t2272,plain,
divide(divide(identity,e),a) = c,
inference(orient,[status(thm)],[t5892]) ).
cnf(t2276,plain,
true = less_equal(c,divide(identity,e)),
inference(cp,[status(thm)],[t57,t2272]) ).
cnf(t2290,plain,
less_equal(c,divide(identity,e)) = true,
inference(orient,[status(thm)],[t2276]) ).
cnf(t2291,plain,
divide(identity,e) = ifeq(true,true,ifeq(less_equal(divide(identity,e),c),true,c,divide(identity,e)),divide(identity,e)),
inference(cp,[status(thm)],[t19,t2290]) ).
cnf(t5893,plain,
divide(identity,e) = ifeq(less_equal(divide(identity,e),c),true,c,divide(identity,e)),
inference(step,[status(thm)],[t2291,t18]) ).
cnf(t452,plain,
zero = divide(divide(divide(divide(X1,e),c),zero),divide(zero,c)),
inference(cp,[status(thm)],[t242,t443]) ).
cnf(t5777,plain,
zero = divide(divide(divide(divide(X1,e),c),zero),zero),
inference(step,[status(thm)],[t452,t52]) ).
cnf(t520,plain,
divide(divide(divide(divide(X1,e),c),zero),zero) = zero,
inference(orient,[status(thm)],[t5777]) ).
cnf(t522,plain,
true = ifeq(zero,zero,less_equal(divide(divide(divide(X1,e),c),zero),zero),true),
inference(cp,[status(thm)],[t97,t520]) ).
cnf(t5781,plain,
true = less_equal(divide(divide(divide(X1,e),c),zero),zero),
inference(step,[status(thm)],[t522,t18]) ).
cnf(t552,plain,
less_equal(divide(divide(divide(X1,e),c),zero),zero) = true,
inference(orient,[status(thm)],[t5781]) ).
cnf(t553,plain,
zero = ifeq(true,true,divide(divide(divide(X1,e),c),zero),zero),
inference(cp,[status(thm)],[t235,t552]) ).
cnf(t5783,plain,
zero = divide(divide(divide(X1,e),c),zero),
inference(step,[status(thm)],[t553,t18]) ).
cnf(t584,plain,
divide(divide(divide(X1,e),c),zero) = zero,
inference(orient,[status(thm)],[t5783]) ).
cnf(t586,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,e),c),zero),true),
inference(cp,[status(thm)],[t97,t584]) ).
cnf(t5784,plain,
true = less_equal(divide(divide(X1,e),c),zero),
inference(step,[status(thm)],[t586,t18]) ).
cnf(t595,plain,
less_equal(divide(divide(X1,e),c),zero) = true,
inference(orient,[status(thm)],[t5784]) ).
cnf(t596,plain,
zero = ifeq(true,true,divide(divide(X1,e),c),zero),
inference(cp,[status(thm)],[t235,t595]) ).
cnf(t5785,plain,
zero = divide(divide(X1,e),c),
inference(step,[status(thm)],[t596,t18]) ).
cnf(t600,plain,
divide(divide(X1,e),c) = zero,
inference(orient,[status(thm)],[t5785]) ).
cnf(t602,plain,
true = ifeq(zero,zero,less_equal(divide(X1,e),c),true),
inference(cp,[status(thm)],[t97,t600]) ).
cnf(t5786,plain,
true = less_equal(divide(X1,e),c),
inference(step,[status(thm)],[t602,t18]) ).
cnf(t611,plain,
less_equal(divide(X1,e),c) = true,
inference(orient,[status(thm)],[t5786]) ).
cnf(t5894,plain,
divide(identity,e) = ifeq(true,true,c,divide(identity,e)),
inference(step,[status(thm)],[t5893,t611]) ).
cnf(t5895,plain,
divide(identity,e) = c,
inference(step,[status(thm)],[t5894,t18]) ).
cnf(t2293,plain,
divide(identity,e) = c,
inference(orient,[status(thm)],[t5895]) ).
cnf(t2294,plain,
true = less_equal(c,divide(c,e)),
inference(cp,[status(thm)],[t454,t2293]) ).
cnf(t2308,plain,
less_equal(c,divide(c,e)) = true,
inference(orient,[status(thm)],[t2294]) ).
cnf(t2311,plain,
divide(c,e) = ifeq(true,true,ifeq(less_equal(divide(c,e),c),true,c,divide(c,e)),divide(c,e)),
inference(cp,[status(thm)],[t19,t2308]) ).
cnf(t5896,plain,
divide(c,e) = ifeq(less_equal(divide(c,e),c),true,c,divide(c,e)),
inference(step,[status(thm)],[t2311,t18]) ).
cnf(t5897,plain,
divide(c,e) = ifeq(true,true,c,divide(c,e)),
inference(step,[status(thm)],[t5896,t611]) ).
cnf(t5898,plain,
divide(c,e) = c,
inference(step,[status(thm)],[t5897,t18]) ).
cnf(t2313,plain,
divide(c,e) = c,
inference(orient,[status(thm)],[t5898]) ).
cnf(t3083,plain,
zero = divide(divide(c,divide(d,e)),g),
inference(cp,[status(thm)],[t3081,t2313]) ).
cnf(t3117,plain,
divide(divide(c,divide(d,e)),g) = zero,
inference(orient,[status(thm)],[t3083]) ).
cnf(t3126,plain,
zero = divide(divide(divide(c,g),divide(divide(d,e),g)),zero),
inference(cp,[status(thm)],[t24,t3117]) ).
cnf(t6001,plain,
zero = divide(divide(c,g),divide(divide(d,e),g)),
inference(step,[status(thm)],[t3126,t2256]) ).
cnf(t3691,plain,
divide(divide(c,g),divide(divide(d,e),g)) = zero,
inference(orient,[status(thm)],[t6001]) ).
cnf(t4920,plain,
divide(divide(c,g),divide(d,e)) = divide(zero,divide(d,e)),
inference(cp,[status(thm)],[t4914,t3691]) ).
cnf(t6132,plain,
divide(divide(c,g),divide(d,e)) = zero,
inference(step,[status(thm)],[t4920,t52]) ).
cnf(t5211,plain,
divide(divide(c,g),divide(d,e)) = zero,
inference(orient,[status(thm)],[t6132]) ).
cnf(t5213,plain,
true = ifeq(zero,zero,less_equal(divide(c,g),divide(d,e)),true),
inference(cp,[status(thm)],[t97,t5211]) ).
cnf(t6158,plain,
true = less_equal(divide(c,g),divide(d,e)),
inference(step,[status(thm)],[t5213,t18]) ).
cnf(t5642,plain,
less_equal(divide(c,g),divide(d,e)) = true,
inference(orient,[status(thm)],[t6158]) ).
cnf(t5643,plain,
divide(d,e) = ifeq(true,true,ifeq(less_equal(divide(d,e),divide(c,g)),true,divide(c,g),divide(d,e)),divide(d,e)),
inference(cp,[status(thm)],[t19,t5642]) ).
cnf(t6159,plain,
divide(d,e) = ifeq(less_equal(divide(d,e),divide(c,g)),true,divide(c,g),divide(d,e)),
inference(step,[status(thm)],[t5643,t18]) ).
cnf(t2537,plain,
zero = divide(divide(divide(divide(X1,c),X2),e),zero),
inference(cp,[status(thm)],[t2512,t191]) ).
cnf(t5915,plain,
zero = divide(divide(divide(X1,c),X2),e),
inference(step,[status(thm)],[t2537,t2256]) ).
cnf(t2612,plain,
divide(divide(divide(X1,c),X2),e) = zero,
inference(orient,[status(thm)],[t5915]) ).
cnf(t2621,plain,
zero = divide(divide(divide(divide(X1,X2),divide(c,X2)),e),zero),
inference(cp,[status(thm)],[t2377,t2612]) ).
cnf(t5951,plain,
zero = divide(divide(divide(X1,X2),divide(c,X2)),e),
inference(step,[status(thm)],[t2621,t2256]) ).
cnf(t3165,plain,
divide(divide(divide(X1,X2),divide(c,X2)),e) = zero,
inference(orient,[status(thm)],[t5951]) ).
cnf(t226,plain,
true = less_equal(divide(divide(X1,g),divide(d,g)),zero),
inference(cp,[status(thm)],[t64,t222]) ).
cnf(t457,plain,
less_equal(divide(divide(X1,g),divide(d,g)),zero) = true,
inference(orient,[status(thm)],[t226]) ).
cnf(t458,plain,
zero = ifeq(true,true,divide(divide(X1,g),divide(d,g)),zero),
inference(cp,[status(thm)],[t235,t457]) ).
cnf(t5769,plain,
zero = divide(divide(X1,g),divide(d,g)),
inference(step,[status(thm)],[t458,t18]) ).
cnf(t464,plain,
divide(divide(X1,g),divide(d,g)) = zero,
inference(orient,[status(thm)],[t5769]) ).
cnf(t466,plain,
true = ifeq(zero,zero,less_equal(divide(X1,g),divide(d,g)),true),
inference(cp,[status(thm)],[t97,t464]) ).
cnf(t5770,plain,
true = less_equal(divide(X1,g),divide(d,g)),
inference(step,[status(thm)],[t466,t18]) ).
cnf(t475,plain,
less_equal(divide(X1,g),divide(d,g)) = true,
inference(orient,[status(thm)],[t5770]) ).
cnf(t45,plain,
zero = divide(divide(d,divide(X1,b)),divide(divide(identity,X1),b)),
inference(cp,[status(thm)],[t24,t44]) ).
cnf(t1266,plain,
divide(divide(d,divide(X1,b)),divide(divide(identity,X1),b)) = zero,
inference(orient,[status(thm)],[t45]) ).
cnf(t77,plain,
true = less_equal(divide(divide(X1,b),d),divide(divide(X1,identity),b)),
inference(cp,[status(thm)],[t64,t44]) ).
cnf(t5713,plain,
true = less_equal(divide(divide(X1,b),d),divide(zero,b)),
inference(step,[status(thm)],[t77,t20]) ).
cnf(t5714,plain,
true = less_equal(divide(divide(X1,b),d),zero),
inference(step,[status(thm)],[t5713,t52]) ).
cnf(t141,plain,
less_equal(divide(divide(X1,b),d),zero) = true,
inference(orient,[status(thm)],[t5714]) ).
cnf(t145,plain,
zero = ifeq(true,true,ifeq(less_equal(zero,divide(divide(X1,b),d)),true,divide(divide(X1,b),d),zero),zero),
inference(cp,[status(thm)],[t19,t141]) ).
cnf(t5719,plain,
zero = ifeq(less_equal(zero,divide(divide(X1,b),d)),true,divide(divide(X1,b),d),zero),
inference(step,[status(thm)],[t145,t18]) ).
cnf(t5720,plain,
zero = ifeq(true,true,divide(divide(X1,b),d),zero),
inference(step,[status(thm)],[t5719,t94]) ).
cnf(t5721,plain,
zero = divide(divide(X1,b),d),
inference(step,[status(thm)],[t5720,t18]) ).
cnf(t160,plain,
divide(divide(X1,b),d) = zero,
inference(orient,[status(thm)],[t5721]) ).
cnf(t164,plain,
true = less_equal(divide(divide(X1,d),divide(b,d)),zero),
inference(cp,[status(thm)],[t64,t160]) ).
cnf(t383,plain,
less_equal(divide(divide(X1,d),divide(b,d)),zero) = true,
inference(orient,[status(thm)],[t164]) ).
cnf(t384,plain,
true = less_equal(divide(g,divide(b,d)),zero),
inference(cp,[status(thm)],[t383,t40]) ).
cnf(t391,plain,
less_equal(divide(g,divide(b,d)),zero) = true,
inference(orient,[status(thm)],[t384]) ).
cnf(t392,plain,
zero = ifeq(true,true,divide(g,divide(b,d)),zero),
inference(cp,[status(thm)],[t235,t391]) ).
cnf(t5760,plain,
zero = divide(g,divide(b,d)),
inference(step,[status(thm)],[t392,t18]) ).
cnf(t398,plain,
divide(g,divide(b,d)) = zero,
inference(orient,[status(thm)],[t5760]) ).
cnf(t400,plain,
true = ifeq(zero,zero,less_equal(g,divide(b,d)),true),
inference(cp,[status(thm)],[t97,t398]) ).
cnf(t5761,plain,
true = less_equal(g,divide(b,d)),
inference(step,[status(thm)],[t400,t18]) ).
cnf(t407,plain,
less_equal(g,divide(b,d)) = true,
inference(orient,[status(thm)],[t5761]) ).
cnf(t408,plain,
divide(b,d) = ifeq(true,true,ifeq(less_equal(divide(b,d),g),true,g,divide(b,d)),divide(b,d)),
inference(cp,[status(thm)],[t19,t407]) ).
cnf(t5762,plain,
divide(b,d) = ifeq(less_equal(divide(b,d),g),true,g,divide(b,d)),
inference(step,[status(thm)],[t408,t18]) ).
cnf(t224,plain,
true = ifeq(zero,zero,less_equal(divide(X1,d),g),true),
inference(cp,[status(thm)],[t97,t222]) ).
cnf(t5742,plain,
true = less_equal(divide(X1,d),g),
inference(step,[status(thm)],[t224,t18]) ).
cnf(t231,plain,
less_equal(divide(X1,d),g) = true,
inference(orient,[status(thm)],[t5742]) ).
cnf(t5763,plain,
divide(b,d) = ifeq(true,true,g,divide(b,d)),
inference(step,[status(thm)],[t5762,t231]) ).
cnf(t5764,plain,
divide(b,d) = g,
inference(step,[status(thm)],[t5763,t18]) ).
cnf(t410,plain,
divide(b,d) = g,
inference(orient,[status(thm)],[t5764]) ).
cnf(t411,plain,
zero = divide(g,b),
inference(cp,[status(thm)],[t21,t410]) ).
cnf(t421,plain,
divide(g,b) = zero,
inference(orient,[status(thm)],[t411]) ).
cnf(t1268,plain,
zero = divide(divide(d,zero),divide(divide(identity,g),b)),
inference(cp,[status(thm)],[t1266,t421]) ).
cnf(t1289,plain,
divide(divide(d,zero),divide(divide(identity,g),b)) = zero,
inference(orient,[status(thm)],[t1268]) ).
cnf(t1291,plain,
true = ifeq(zero,zero,less_equal(divide(d,zero),divide(divide(identity,g),b)),true),
inference(cp,[status(thm)],[t97,t1289]) ).
cnf(t5834,plain,
true = less_equal(divide(d,zero),divide(divide(identity,g),b)),
inference(step,[status(thm)],[t1291,t18]) ).
cnf(t1342,plain,
less_equal(divide(d,zero),divide(divide(identity,g),b)) = true,
inference(orient,[status(thm)],[t5834]) ).
cnf(t5884,plain,
less_equal(d,divide(divide(identity,g),b)) = true,
inference(step,[status(thm)],[t1342,t2256]) ).
cnf(t2260,plain,
less_equal(d,divide(divide(identity,g),b)) = true,
inference(rw,[status(thm)],[t5884]) ).
cnf(t2318,plain,
less_equal(d,divide(divide(identity,g),b)) = true,
inference(orient,[status(thm)],[t2260]) ).
cnf(t2321,plain,
divide(divide(identity,g),b) = ifeq(true,true,ifeq(less_equal(divide(divide(identity,g),b),d),true,d,divide(divide(identity,g),b)),divide(divide(identity,g),b)),
inference(cp,[status(thm)],[t19,t2318]) ).
cnf(t5899,plain,
divide(divide(identity,g),b) = ifeq(less_equal(divide(divide(identity,g),b),d),true,d,divide(divide(identity,g),b)),
inference(step,[status(thm)],[t2321,t18]) ).
cnf(t162,plain,
true = ifeq(zero,zero,less_equal(divide(X1,b),d),true),
inference(cp,[status(thm)],[t97,t160]) ).
cnf(t5722,plain,
true = less_equal(divide(X1,b),d),
inference(step,[status(thm)],[t162,t18]) ).
cnf(t169,plain,
less_equal(divide(X1,b),d) = true,
inference(orient,[status(thm)],[t5722]) ).
cnf(t5900,plain,
divide(divide(identity,g),b) = ifeq(true,true,d,divide(divide(identity,g),b)),
inference(step,[status(thm)],[t5899,t169]) ).
cnf(t5901,plain,
divide(divide(identity,g),b) = d,
inference(step,[status(thm)],[t5900,t18]) ).
cnf(t2323,plain,
divide(divide(identity,g),b) = d,
inference(orient,[status(thm)],[t5901]) ).
cnf(t2327,plain,
true = less_equal(d,divide(identity,g)),
inference(cp,[status(thm)],[t57,t2323]) ).
cnf(t2341,plain,
less_equal(d,divide(identity,g)) = true,
inference(orient,[status(thm)],[t2327]) ).
cnf(t2342,plain,
divide(identity,g) = ifeq(true,true,ifeq(less_equal(divide(identity,g),d),true,d,divide(identity,g)),divide(identity,g)),
inference(cp,[status(thm)],[t19,t2341]) ).
cnf(t5902,plain,
divide(identity,g) = ifeq(less_equal(divide(identity,g),d),true,d,divide(identity,g)),
inference(step,[status(thm)],[t2342,t18]) ).
cnf(t473,plain,
zero = divide(divide(divide(divide(X1,g),d),zero),divide(zero,d)),
inference(cp,[status(thm)],[t242,t464]) ).
cnf(t5778,plain,
zero = divide(divide(divide(divide(X1,g),d),zero),zero),
inference(step,[status(thm)],[t473,t52]) ).
cnf(t528,plain,
divide(divide(divide(divide(X1,g),d),zero),zero) = zero,
inference(orient,[status(thm)],[t5778]) ).
cnf(t530,plain,
true = ifeq(zero,zero,less_equal(divide(divide(divide(X1,g),d),zero),zero),true),
inference(cp,[status(thm)],[t97,t528]) ).
cnf(t5787,plain,
true = less_equal(divide(divide(divide(X1,g),d),zero),zero),
inference(step,[status(thm)],[t530,t18]) ).
cnf(t614,plain,
less_equal(divide(divide(divide(X1,g),d),zero),zero) = true,
inference(orient,[status(thm)],[t5787]) ).
cnf(t615,plain,
zero = ifeq(true,true,divide(divide(divide(X1,g),d),zero),zero),
inference(cp,[status(thm)],[t235,t614]) ).
cnf(t5788,plain,
zero = divide(divide(divide(X1,g),d),zero),
inference(step,[status(thm)],[t615,t18]) ).
cnf(t619,plain,
divide(divide(divide(X1,g),d),zero) = zero,
inference(orient,[status(thm)],[t5788]) ).
cnf(t621,plain,
true = ifeq(zero,zero,less_equal(divide(divide(X1,g),d),zero),true),
inference(cp,[status(thm)],[t97,t619]) ).
cnf(t5789,plain,
true = less_equal(divide(divide(X1,g),d),zero),
inference(step,[status(thm)],[t621,t18]) ).
cnf(t630,plain,
less_equal(divide(divide(X1,g),d),zero) = true,
inference(orient,[status(thm)],[t5789]) ).
cnf(t631,plain,
zero = ifeq(true,true,divide(divide(X1,g),d),zero),
inference(cp,[status(thm)],[t235,t630]) ).
cnf(t5790,plain,
zero = divide(divide(X1,g),d),
inference(step,[status(thm)],[t631,t18]) ).
cnf(t635,plain,
divide(divide(X1,g),d) = zero,
inference(orient,[status(thm)],[t5790]) ).
cnf(t637,plain,
true = ifeq(zero,zero,less_equal(divide(X1,g),d),true),
inference(cp,[status(thm)],[t97,t635]) ).
cnf(t5791,plain,
true = less_equal(divide(X1,g),d),
inference(step,[status(thm)],[t637,t18]) ).
cnf(t646,plain,
less_equal(divide(X1,g),d) = true,
inference(orient,[status(thm)],[t5791]) ).
cnf(t5903,plain,
divide(identity,g) = ifeq(true,true,d,divide(identity,g)),
inference(step,[status(thm)],[t5902,t646]) ).
cnf(t5904,plain,
divide(identity,g) = d,
inference(step,[status(thm)],[t5903,t18]) ).
cnf(t2344,plain,
divide(identity,g) = d,
inference(orient,[status(thm)],[t5904]) ).
cnf(t2345,plain,
true = less_equal(d,divide(d,g)),
inference(cp,[status(thm)],[t475,t2344]) ).
cnf(t2359,plain,
less_equal(d,divide(d,g)) = true,
inference(orient,[status(thm)],[t2345]) ).
cnf(t2362,plain,
divide(d,g) = ifeq(true,true,ifeq(less_equal(divide(d,g),d),true,d,divide(d,g)),divide(d,g)),
inference(cp,[status(thm)],[t19,t2359]) ).
cnf(t5905,plain,
divide(d,g) = ifeq(less_equal(divide(d,g),d),true,d,divide(d,g)),
inference(step,[status(thm)],[t2362,t18]) ).
cnf(t5906,plain,
divide(d,g) = ifeq(true,true,d,divide(d,g)),
inference(step,[status(thm)],[t5905,t646]) ).
cnf(t5907,plain,
divide(d,g) = d,
inference(step,[status(thm)],[t5906,t18]) ).
cnf(t2364,plain,
divide(d,g) = d,
inference(orient,[status(thm)],[t5907]) ).
cnf(t3167,plain,
zero = divide(divide(d,divide(c,g)),e),
inference(cp,[status(thm)],[t3165,t2364]) ).
cnf(t3201,plain,
divide(divide(d,divide(c,g)),e) = zero,
inference(orient,[status(thm)],[t3167]) ).
cnf(t3210,plain,
zero = divide(divide(divide(d,e),divide(divide(c,g),e)),zero),
inference(cp,[status(thm)],[t24,t3201]) ).
cnf(t6009,plain,
zero = divide(divide(d,e),divide(divide(c,g),e)),
inference(step,[status(thm)],[t3210,t2256]) ).
cnf(t3775,plain,
divide(divide(d,e),divide(divide(c,g),e)) = zero,
inference(orient,[status(thm)],[t6009]) ).
cnf(t4917,plain,
divide(divide(d,e),divide(c,g)) = divide(zero,divide(c,g)),
inference(cp,[status(thm)],[t4914,t3775]) ).
cnf(t6129,plain,
divide(divide(d,e),divide(c,g)) = zero,
inference(step,[status(thm)],[t4917,t52]) ).
cnf(t5169,plain,
divide(divide(d,e),divide(c,g)) = zero,
inference(orient,[status(thm)],[t6129]) ).
cnf(t5171,plain,
true = ifeq(zero,zero,less_equal(divide(d,e),divide(c,g)),true),
inference(cp,[status(thm)],[t97,t5169]) ).
cnf(t6155,plain,
true = less_equal(divide(d,e),divide(c,g)),
inference(step,[status(thm)],[t5171,t18]) ).
cnf(t5633,plain,
less_equal(divide(d,e),divide(c,g)) = true,
inference(orient,[status(thm)],[t6155]) ).
cnf(t6160,plain,
divide(d,e) = ifeq(true,true,divide(c,g),divide(d,e)),
inference(step,[status(thm)],[t6159,t5633]) ).
cnf(t6161,plain,
divide(d,e) = divide(c,g),
inference(step,[status(thm)],[t6160,t18]) ).
cnf(t5645,plain,
divide(c,g) = divide(d,e),
inference(orient,[status(thm)],[t6161]) ).
cnf(t6164,plain,
ifeq(divide(d,e),divide(d,e),false,true) = true,
inference(step,[status(thm)],[t102,t5645]) ).
cnf(t6165,plain,
false = true,
inference(step,[status(thm)],[t6164,t18]) ).
cnf(t5680,plain,
false = true,
inference(rw,[status(thm)],[t6165]) ).
cnf(t5694,plain,
false = true,
inference(orient,[status(thm)],[t5680]) ).
cnf(f12,negated_conjecture,
divide(c,g) != divide(d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_commutativity) ).
fof(f12_nnf,plain,
divide(c,g) != divide(d,e),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
divide(c,g) != divide(d,e),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
divide(c,g) != divide(d,e),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7,c12]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5694]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HEN011-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.04/5.31 % Computer : n012.cluster.edu
% 0.04/5.31 % Model : x86_64 x86_64
% 0.04/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.31 % Memory : 8046.5625MB
% 0.04/5.31 % OS : Linux 6.8.0-71-generic
% 0.04/5.31 % CPULimit : 300
% 0.04/5.31 % WCLimit : 300
% 0.04/5.31 % DateTime : Wed Sep 23 16:17:26 UTC 2026
% 0.04/5.31 % CPUTime :
% 0.04/5.31 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.02/6.49 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.02/6.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------