%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM477+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:20:08 PM UTC 2026
% Result : Theorem 64.55s 13.56s
% Output : Proof 64.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 10
% Syntax : Number of formulae : 74 ( 52 unt; 0 def)
% Number of atoms : 117 ( 73 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 73 ( 30 ~; 17 |; 23 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-4 aty)
% Number of variables : 38 ( 2 sgn 11 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,hypothesis,
( xn != sz00
& doDivides0(xm,xn)
& ? [W0] :
( xn = sdtasdt0(xm,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1494_04) ).
fof(f35_nnf,plain,
( xn != sz00
& doDivides0(xm,xn)
& ? [W0] :
( xn = sdtasdt0(xm,W0)
& aNaturalNumber0(W0) ) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( xn != sz00
& doDivides0(xm,xn)
& xn = sdtasdt0(xm,sk2)
& aNaturalNumber0(sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f35_nnf]) ).
cnf(c63,plain,
xn != sz00,
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t22,plain,
eq(xn,sz00) = false,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(t5446,plain,
eq(xn,sz00) = false,
inference(orient,[status(thm)],[t22]) ).
cnf(c61,plain,
xn = sdtasdt0(xm,sk2),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t39,plain,
sdtasdt0(xm,sk2) = xn,
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(t4700,plain,
sdtasdt0(xm,sk2) = xn,
inference(orient,[status(thm)],[t39]) ).
cnf(t158,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t271,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t158]) ).
fof(f26,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul2) ).
fof(f26_nnf,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [W0,W1] :
( sdtlseqdt0(W1,sdtasdt0(W1,W0))
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c46,plain,
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t218,plain,
ifeq(aNaturalNumber0(X1),true,ifeq(aNaturalNumber0(X2),true,or(eq(X1,sz00),sdtlseqdt0(X2,sdtasdt0(X2,X1))),true),true) = true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t310,plain,
ifeq(aNaturalNumber0(X1),true,ifeq(aNaturalNumber0(X2),true,or(eq(X1,sz00),sdtlseqdt0(X2,sdtasdt0(X2,X1))),true),true) = true,
inference(orient,[status(thm)],[t218]) ).
cnf(t4719,plain,
true = ifeq(aNaturalNumber0(sk2),true,ifeq(aNaturalNumber0(xm),true,or(eq(sk2,sz00),sdtlseqdt0(xm,xn)),true),true),
inference(cp,[status(thm)],[t310,t4700]) ).
cnf(c60,plain,
aNaturalNumber0(sk2),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t0,plain,
aNaturalNumber0(sk2) = true,
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(t1568,plain,
aNaturalNumber0(sk2) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t39273,plain,
true = ifeq(true,true,ifeq(aNaturalNumber0(xm),true,or(eq(sk2,sz00),sdtlseqdt0(xm,xn)),true),true),
inference(step,[status(thm)],[t4719,t1568]) ).
cnf(t88,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t88]) ).
cnf(t39274,plain,
true = ifeq(aNaturalNumber0(xm),true,or(eq(sk2,sz00),sdtlseqdt0(xm,xn)),true),
inference(step,[status(thm)],[t39273,t256]) ).
fof(f34,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1494) ).
fof(f34_nnf,plain,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c58,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t3,plain,
aNaturalNumber0(xm) = true,
inference(equality_encoding,[status(esa)],[c58]) ).
cnf(t416,plain,
aNaturalNumber0(xm) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t39275,plain,
true = ifeq(true,true,or(eq(sk2,sz00),sdtlseqdt0(xm,xn)),true),
inference(step,[status(thm)],[t39274,t416]) ).
cnf(t39276,plain,
true = or(eq(sk2,sz00),sdtlseqdt0(xm,xn)),
inference(step,[status(thm)],[t39275,t256]) ).
fof(f36,conjecture,
( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f36_neg,negated_conjecture,
~ ( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f36_nnf,plain,
( ~ sdtlseqdt0(xm,xn)
& ! [W0] :
( sdtpldt0(xm,W0) != xn
| ~ aNaturalNumber0(W0) ) ),
inference(nnf_transformation,[status(thm)],[f36_neg]) ).
fof(f36_sk,plain,
! [W0] :
( ~ sdtlseqdt0(xm,xn)
& ( sdtpldt0(xm,W0) != xn
| ~ aNaturalNumber0(W0) ) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c65,plain,
~ sdtlseqdt0(xm,xn),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t52,plain,
sdtlseqdt0(xm,xn) = false,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t5499,plain,
sdtlseqdt0(xm,xn) = false,
inference(orient,[status(thm)],[t52]) ).
cnf(t39277,plain,
true = or(eq(sk2,sz00),false),
inference(step,[status(thm)],[t39276,t5499]) ).
cnf(t23,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t272,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t23]) ).
cnf(t39278,plain,
true = eq(sk2,sz00),
inference(step,[status(thm)],[t39277,t272]) ).
cnf(t36936,plain,
eq(sk2,sz00) = true,
inference(orient,[status(thm)],[t39278]) ).
cnf(t36937,plain,
sz00 = ifeq(true,true,sk2,sz00),
inference(cp,[status(thm)],[t271,t36936]) ).
cnf(t39279,plain,
sz00 = sk2,
inference(step,[status(thm)],[t36937,t256]) ).
cnf(t36961,plain,
sk2 = sz00,
inference(orient,[status(thm)],[t39279]) ).
cnf(t39281,plain,
sdtasdt0(xm,sz00) = xn,
inference(step,[status(thm)],[t4700,t36961]) ).
fof(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulZero) ).
fof(f11_nnf,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c14,plain,
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi12,axiom,
ifeq(aNaturalNumber0(X0),true,sdtasdt0(X0,sz00),sz00) = sz00,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(hi55,axiom,
aNaturalNumber0(xm) = true,
inference(equality_encoding,[status(esa)],[c58]) ).
cnf(t40,plain,
sdtasdt0(xm,sz00) = sz00,
inference(hyper_resolution,[status(thm)],[hi12,hi55]) ).
cnf(t3300,plain,
sdtasdt0(xm,sz00) = sz00,
inference(orient,[status(thm)],[t40]) ).
cnf(t39282,plain,
sz00 = xn,
inference(step,[status(thm)],[t39281,t3300]) ).
cnf(t36963,plain,
sz00 = xn,
inference(rw,[status(thm)],[t39282]) ).
cnf(t36984,plain,
sz00 = xn,
inference(orient,[status(thm)],[t36963]) ).
cnf(t39349,plain,
eq(xn,xn) = false,
inference(step,[status(thm)],[t5446,t36984]) ).
cnf(t20,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t2207,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t39350,plain,
true = false,
inference(step,[status(thm)],[t39349,t2207]) ).
cnf(t37006,plain,
true = false,
inference(rw,[status(thm)],[t39350]) ).
cnf(t37218,plain,
false = true,
inference(orient,[status(thm)],[t37006]) ).
fof(f2,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f2_nnf,plain,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c3,plain,
sz10 != sz00,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(c64,plain,
( sdtpldt0(xm,X0) != xn
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c3,c63,c64,c65]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t37218]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM477+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n014.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Thu Sep 24 04:11:24 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 64.55/13.56 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.55/13.56 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------