%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG046+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:37:35 PM UTC 2026
% Result : Theorem 229.18s 39.91s
% Output : Proof 229.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 10
% Syntax : Number of formulae : 87 ( 59 unt; 0 def)
% Number of atoms : 168 ( 106 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 123 ( 42 ~; 32 |; 43 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-4 aty)
% Number of variables : 63 ( 4 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,conjecture,
sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xx,xy),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f18_neg,negated_conjecture,
sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f18_nnf,plain,
sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy),
inference(nnf_transformation,[status(thm)],[f18_neg]) ).
fof(f18_sk,plain,
sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c33,plain,
sdtasdt0(smndt0(xx),smndt0(xy)) != sdtasdt0(xx,xy),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t232,plain,
eq(sdtasdt0(smndt0(xx),smndt0(xy)),sdtasdt0(xx,xy)) = false,
inference(equality_encoding,[status(esa)],[c33]) ).
fof(f13,axiom,
! [W0,W1,W2] :
( ( aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
& sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(f13_nnf,plain,
! [W0,W1,W2] :
( ( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
& sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) )
| ~ aScalar0(W2)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [W0,W1,W2] :
( ( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
& sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
& sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
& sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) )
| ~ aScalar0(W2)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c25,plain,
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi21,axiom,
ifeq(aScalar0(X0),true,ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,sdtasdt0(X0,X1),sdtasdt0(X1,X0)),sdtasdt0(X1,X0)),sdtasdt0(X1,X0)) = sdtasdt0(X1,X0),
inference(equality_encoding,[status(esa)],[c25]) ).
fof(f17,hypothesis,
( aScalar0(xy)
& aScalar0(xx) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__799) ).
fof(f17_nnf,plain,
( aScalar0(xy)
& aScalar0(xx) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( aScalar0(xy)
& aScalar0(xx) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c32,plain,
aScalar0(xy),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi28,axiom,
aScalar0(xy) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(c31,plain,
aScalar0(xx),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi27,axiom,
aScalar0(xx) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t129,plain,
sdtasdt0(xy,xx) = sdtasdt0(xx,xy),
inference(hyper_resolution,[status(thm)],[hi21,hi28,hi27,hi28]) ).
cnf(t478,plain,
sdtasdt0(xx,xy) = sdtasdt0(xy,xx),
inference(orient,[status(thm)],[t129]) ).
cnf(t221465,plain,
eq(sdtasdt0(smndt0(xx),smndt0(xy)),sdtasdt0(xy,xx)) = false,
inference(step,[status(thm)],[t232,t478]) ).
cnf(t2258,plain,
eq(sdtasdt0(smndt0(xx),smndt0(xy)),sdtasdt0(xy,xx)) = false,
inference(orient,[status(thm)],[t221465]) ).
fof(f16,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1))
& sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMNeg) ).
fof(f16_nnf,plain,
! [W0,W1] :
( ( sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1))
& sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) )
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [W0,W1] :
( ( sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1))
& sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) )
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c29,plain,
( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t247,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,sdtasdt0(X1,smndt0(X2)),smndt0(sdtasdt0(X1,X2))),smndt0(sdtasdt0(X1,X2))) = smndt0(sdtasdt0(X1,X2)),
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t556,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,sdtasdt0(X1,smndt0(X2)),smndt0(sdtasdt0(X1,X2))),smndt0(sdtasdt0(X1,X2))) = smndt0(sdtasdt0(X1,X2)),
inference(orient,[status(thm)],[t247]) ).
fof(f11,axiom,
! [W0] :
( aScalar0(W0)
=> aScalar0(smndt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNegSc) ).
fof(f11_nnf,plain,
! [W0] :
( aScalar0(smndt0(W0))
| ~ aScalar0(W0) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [W0] :
( aScalar0(smndt0(W0))
| ~ aScalar0(W0) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c13,plain,
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi9,axiom,
ifeq(aScalar0(X0),true,aScalar0(smndt0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h78,plain,
aScalar0(smndt0(xx)) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi27]) ).
cnf(t159,plain,
sdtasdt0(xy,smndt0(xx)) = sdtasdt0(smndt0(xx),xy),
inference(hyper_resolution,[status(thm)],[hi21,h78,hi28,h78]) ).
cnf(t497,plain,
sdtasdt0(smndt0(xx),xy) = sdtasdt0(xy,smndt0(xx)),
inference(orient,[status(thm)],[t159]) ).
cnf(t572,plain,
smndt0(sdtasdt0(smndt0(xx),xy)) = ifeq(aScalar0(smndt0(xx)),true,ifeq(aScalar0(xy),true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),smndt0(sdtasdt0(smndt0(xx),xy))),
inference(cp,[status(thm)],[t556,t497]) ).
cnf(t226294,plain,
smndt0(sdtasdt0(xy,smndt0(xx))) = ifeq(aScalar0(smndt0(xx)),true,ifeq(aScalar0(xy),true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),smndt0(sdtasdt0(smndt0(xx),xy))),
inference(step,[status(thm)],[t572,t497]) ).
fof(f10,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> aScalar0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f10_nnf,plain,
! [W0,W1] :
( aScalar0(sdtasdt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [W0,W1] :
( aScalar0(sdtasdt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c12,plain,
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi8,axiom,
ifeq(aScalar0(X0),true,ifeq(aScalar0(X1),true,aScalar0(sdtasdt0(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h251,plain,
aScalar0(sdtasdt0(xy,xx)) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi28,hi27]) ).
fof(f12,axiom,
! [W0] :
( aScalar0(W0)
=> ( smndt0(sz0z00) = sz0z00
& smndt0(smndt0(W0)) = W0
& sdtpldt0(smndt0(W0),W0) = sz0z00
& sdtpldt0(W0,smndt0(W0)) = sz0z00
& sdtasdt0(sz0z00,W0) = sz0z00
& sdtasdt0(W0,sz0z00) = sz0z00
& sdtpldt0(sz0z00,W0) = W0
& sdtpldt0(W0,sz0z00) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mScZero) ).
fof(f12_nnf,plain,
! [W0] :
( ( smndt0(sz0z00) = sz0z00
& smndt0(smndt0(W0)) = W0
& sdtpldt0(smndt0(W0),W0) = sz0z00
& sdtpldt0(W0,smndt0(W0)) = sz0z00
& sdtasdt0(sz0z00,W0) = sz0z00
& sdtasdt0(W0,sz0z00) = sz0z00
& sdtpldt0(sz0z00,W0) = W0
& sdtpldt0(W0,sz0z00) = W0 )
| ~ aScalar0(W0) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [W0] :
( ( smndt0(sz0z00) = sz0z00
& smndt0(smndt0(W0)) = W0
& sdtpldt0(smndt0(W0),W0) = sz0z00
& sdtpldt0(W0,smndt0(W0)) = sz0z00
& sdtasdt0(sz0z00,W0) = sz0z00
& sdtasdt0(W0,sz0z00) = sz0z00
& sdtpldt0(sz0z00,W0) = W0
& sdtpldt0(W0,sz0z00) = W0 )
| ~ aScalar0(W0) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c20,plain,
( smndt0(smndt0(X0)) = X0
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi16,axiom,
ifeq(aScalar0(X0),true,smndt0(smndt0(X0)),X0) = X0,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t211,plain,
smndt0(smndt0(sdtasdt0(xy,xx))) = sdtasdt0(xy,xx),
inference(hyper_resolution,[status(thm)],[hi16,h251]) ).
cnf(c30,plain,
( sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi26,axiom,
ifeq(aScalar0(X0),true,ifeq(aScalar0(X1),true,sdtasdt0(smndt0(X0),X1),smndt0(sdtasdt0(X0,X1))),smndt0(sdtasdt0(X0,X1))) = smndt0(sdtasdt0(X0,X1)),
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t197,plain,
smndt0(sdtasdt0(xx,xy)) = sdtasdt0(smndt0(xx),xy),
inference(hyper_resolution,[status(thm)],[hi26,hi27,hi28]) ).
cnf(t221446,plain,
smndt0(sdtasdt0(xy,xx)) = sdtasdt0(smndt0(xx),xy),
inference(step,[status(thm)],[t197,t478]) ).
cnf(t221447,plain,
smndt0(sdtasdt0(xy,xx)) = sdtasdt0(xy,smndt0(xx)),
inference(step,[status(thm)],[t221446,t497]) ).
cnf(t506,plain,
smndt0(sdtasdt0(xy,xx)) = sdtasdt0(xy,smndt0(xx)),
inference(orient,[status(thm)],[t221447]) ).
cnf(t221456,plain,
smndt0(sdtasdt0(xy,smndt0(xx))) = sdtasdt0(xy,xx),
inference(step,[status(thm)],[t211,t506]) ).
cnf(t537,plain,
smndt0(sdtasdt0(xy,smndt0(xx))) = sdtasdt0(xy,xx),
inference(orient,[status(thm)],[t221456]) ).
cnf(t226295,plain,
sdtasdt0(xy,xx) = ifeq(aScalar0(smndt0(xx)),true,ifeq(aScalar0(xy),true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),smndt0(sdtasdt0(smndt0(xx),xy))),
inference(step,[status(thm)],[t226294,t537]) ).
cnf(t9,plain,
aScalar0(smndt0(xx)) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi27]) ).
cnf(t1862,plain,
aScalar0(smndt0(xx)) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t226296,plain,
sdtasdt0(xy,xx) = ifeq(true,true,ifeq(aScalar0(xy),true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),smndt0(sdtasdt0(smndt0(xx),xy))),
inference(step,[status(thm)],[t226295,t1862]) ).
cnf(t102,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t102]) ).
cnf(t226297,plain,
sdtasdt0(xy,xx) = ifeq(aScalar0(xy),true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),
inference(step,[status(thm)],[t226296,t256]) ).
cnf(h247,plain,
aScalar0(smndt0(xy)) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi28]) ).
cnf(t50,plain,
aScalar0(smndt0(smndt0(xy))) = true,
inference(hyper_resolution,[status(thm)],[hi9,h247]) ).
cnf(t28,plain,
smndt0(smndt0(xy)) = xy,
inference(hyper_resolution,[status(thm)],[hi16,hi28]) ).
cnf(t647,plain,
smndt0(smndt0(xy)) = xy,
inference(orient,[status(thm)],[t28]) ).
cnf(t221461,plain,
aScalar0(xy) = true,
inference(step,[status(thm)],[t50,t647]) ).
cnf(t1889,plain,
aScalar0(xy) = true,
inference(orient,[status(thm)],[t221461]) ).
cnf(t226298,plain,
sdtasdt0(xy,xx) = ifeq(true,true,sdtasdt0(smndt0(xx),smndt0(xy)),smndt0(sdtasdt0(xy,smndt0(xx)))),
inference(step,[status(thm)],[t226297,t1889]) ).
cnf(t226299,plain,
sdtasdt0(xy,xx) = sdtasdt0(smndt0(xx),smndt0(xy)),
inference(step,[status(thm)],[t226298,t256]) ).
cnf(t221374,plain,
sdtasdt0(smndt0(xx),smndt0(xy)) = sdtasdt0(xy,xx),
inference(orient,[status(thm)],[t226299]) ).
cnf(t226300,plain,
eq(sdtasdt0(xy,xx),sdtasdt0(xy,xx)) = false,
inference(step,[status(thm)],[t2258,t221374]) ).
cnf(t11,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t2243,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t226301,plain,
true = false,
inference(step,[status(thm)],[t226300,t2243]) ).
cnf(t221407,plain,
true = false,
inference(rw,[status(thm)],[t226301]) ).
cnf(t221409,plain,
false = true,
inference(orient,[status(thm)],[t221407]) ).
fof(f2,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSuccNat) ).
fof(f2_nnf,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) )
| ~ aNaturalNumber0(W0) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) )
| ~ aNaturalNumber0(W0) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c3,plain,
( szszuzczcdt0(X0) != sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c3,c33]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t221409]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG046+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n011.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 07:57:20 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 229.18/39.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 229.18/39.91 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------