%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM303+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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 02:19:00 PM UTC 2026
% Result : Theorem 210.78s 27.12s
% Output : Proof 210.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 75 ( 62 unt; 0 def)
% Number of atoms : 105 ( 58 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 59 ( 29 ~; 20 |; 7 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-4 aty)
% Number of variables : 93 ( 14 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f280,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> less(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_entry_point_pos_pos) ).
fof(f280_nnf,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(nnf_transformation,[status(thm)],[f280]) ).
fof(f280_sk,plain,
! [X,RDN_X,Y,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(skolemisation,[status(esa)],[f280_nnf]) ).
cnf(c280,plain,
( less(X0,X1)
| ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2)) ),
inference(cnf_transformation,[status(esa)],[f280_sk]) ).
cnf(t217,plain,
ifeq(rdn_translate(X1,rdn_pos(X2)),true,ifeq(rdn_translate(X3,rdn_pos(X4)),true,ifeq(rdn_positive_less(X2,X4),true,less(X1,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c280]) ).
cnf(t349,plain,
ifeq(rdn_translate(X1,rdn_pos(X2)),true,ifeq(rdn_translate(X3,rdn_pos(X4)),true,ifeq(rdn_positive_less(X2,X4),true,less(X1,X3),true),true),true) = true,
inference(orient,[status(thm)],[t217]) ).
fof(f31,axiom,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn31) ).
fof(f31_nnf,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t93,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t718,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))) = true,
inference(orient,[status(thm)],[t93]) ).
cnf(t723,plain,
true = ifeq(rdn_translate(X1,rdn_pos(X2)),true,ifeq(true,true,ifeq(rdn_positive_less(X2,rdn(rdnn(n1),rdnn(n3))),true,less(X1,n31),true),true),true),
inference(cp,[status(thm)],[t349,t718]) ).
cnf(t34,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t219,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t34]) ).
cnf(t22872,plain,
true = ifeq(rdn_translate(X1,rdn_pos(X2)),true,ifeq(rdn_positive_less(X2,rdn(rdnn(n1),rdnn(n3))),true,less(X1,n31),true),true),
inference(step,[status(thm)],[t723,t219]) ).
cnf(t19483,plain,
ifeq(rdn_translate(X1,rdn_pos(X2)),true,ifeq(rdn_positive_less(X2,rdn(rdnn(n1),rdnn(n3))),true,less(X1,n31),true),true) = true,
inference(orient,[status(thm)],[t22872]) ).
fof(f21,axiom,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn21) ).
fof(f21_nnf,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t92,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t724,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))) = true,
inference(orient,[status(thm)],[t92]) ).
fof(f401,conjecture,
n31 != n21,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',n31_not_n12) ).
fof(f401_neg,negated_conjecture,
~ ( n31 != n21 ),
inference(negated_conjecture,[status(cth)],[f401]) ).
fof(f401_nnf,plain,
n31 = n21,
inference(nnf_transformation,[status(thm)],[f401_neg]) ).
cnf(c406,plain,
n31 = n21,
inference(cnf_transformation,[status(esa)],[f401_nnf]) ).
cnf(t0,plain,
n31 = n21,
inference(equality_encoding,[status(esa)],[c406]) ).
cnf(t848,plain,
n21 = n31,
inference(orient,[status(thm)],[t0]) ).
cnf(t20343,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n2)))) = true,
inference(step,[status(thm)],[t724,t848]) ).
cnf(t849,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n2)))) = true,
inference(rw,[status(thm)],[t20343]) ).
cnf(t1151,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n2)))) = true,
inference(orient,[status(thm)],[t849]) ).
cnf(t19484,plain,
true = ifeq(true,true,ifeq(rdn_positive_less(rdn(rdnn(n1),rdnn(n2)),rdn(rdnn(n1),rdnn(n3))),true,less(n31,n31),true),true),
inference(cp,[status(thm)],[t19483,t1151]) ).
cnf(t22873,plain,
true = ifeq(rdn_positive_less(rdn(rdnn(n1),rdnn(n2)),rdn(rdnn(n1),rdnn(n3))),true,less(n31,n31),true),
inference(step,[status(thm)],[t19484,t219]) ).
fof(f275,axiom,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(Os,Ob)
=> rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn_positive_less_multi_digit_high) ).
fof(f275_nnf,plain,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob))
| ~ rdn_positive_less(Os,Ob) ),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [Os,Ob,Ds,Db] :
( rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob))
| ~ rdn_positive_less(Os,Ob) ),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c275,plain,
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(X1,X3) ),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
cnf(t207,plain,
ifeq(rdn_positive_less(X1,X2),true,rdn_positive_less(rdn(rdnn(X3),X1),rdn(rdnn(X4),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c275]) ).
cnf(t346,plain,
ifeq(rdn_positive_less(X1,X2),true,rdn_positive_less(rdn(rdnn(X3),X1),rdn(rdnn(X4),X2)),true) = true,
inference(orient,[status(thm)],[t207]) ).
fof(f267,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn_positive_less23) ).
fof(f267_nnf,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c267,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(t43,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)) = true,
inference(equality_encoding,[status(esa)],[c267]) ).
cnf(t603,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(t604,plain,
true = ifeq(true,true,rdn_positive_less(rdn(rdnn(X1),rdnn(n2)),rdn(rdnn(X2),rdnn(n3))),true),
inference(cp,[status(thm)],[t346,t603]) ).
cnf(t20514,plain,
true = rdn_positive_less(rdn(rdnn(X1),rdnn(n2)),rdn(rdnn(X2),rdnn(n3))),
inference(step,[status(thm)],[t604,t219]) ).
cnf(t1642,plain,
rdn_positive_less(rdn(rdnn(X1),rdnn(n2)),rdn(rdnn(X2),rdnn(n3))) = true,
inference(orient,[status(thm)],[t20514]) ).
cnf(t22874,plain,
true = ifeq(true,true,less(n31,n31),true),
inference(step,[status(thm)],[t22873,t1642]) ).
cnf(t22875,plain,
true = less(n31,n31),
inference(step,[status(thm)],[t22874,t219]) ).
cnf(t61,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t845,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t61]) ).
fof(f283,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f283_nnf,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f283]) ).
fof(f283_sk,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(skolemisation,[status(esa)],[f283_nnf]) ).
cnf(c284,plain,
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
cnf(t99,plain,
or(not(less(X1,X2)),not(eq(X2,X1))) = true,
inference(equality_encoding,[status(esa)],[c284]) ).
cnf(t822,plain,
or(not(less(X1,X2)),not(eq(X2,X1))) = true,
inference(orient,[status(thm)],[t99]) ).
cnf(t3,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t833,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t834,plain,
true = or(not(less(X1,X1)),not(true)),
inference(cp,[status(thm)],[t822,t833]) ).
cnf(t2,plain,
not(true) = false,
introduced(definition) ).
cnf(t846,plain,
not(true) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t20437,plain,
true = or(not(less(X1,X1)),false),
inference(step,[status(thm)],[t834,t846]) ).
cnf(t16,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t233,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(t20438,plain,
true = not(less(X1,X1)),
inference(step,[status(thm)],[t20437,t233]) ).
cnf(t1094,plain,
not(less(X1,X1)) = true,
inference(orient,[status(thm)],[t20438]) ).
cnf(t1095,plain,
false = ifeq(true,true,less(X1,X1),false),
inference(cp,[status(thm)],[t845,t1094]) ).
cnf(t20439,plain,
false = less(X1,X1),
inference(step,[status(thm)],[t1095,t219]) ).
cnf(t1096,plain,
less(X1,X1) = false,
inference(orient,[status(thm)],[t20439]) ).
cnf(t22876,plain,
true = false,
inference(step,[status(thm)],[t22875,t1096]) ).
cnf(t19501,plain,
false = true,
inference(orient,[status(thm)],[t22876]) ).
cnf(c283,plain,
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c283,c284]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t19501]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM303+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 03:32:41 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 210.78/27.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 210.78/27.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------