%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG059+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:37 PM UTC 2026
% Result : Theorem 47.24s 11.44s
% Output : Proof 47.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 13
% Syntax : Number of formulae : 101 ( 69 unt; 0 def)
% Number of atoms : 168 ( 102 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 111 ( 44 ~; 30 |; 31 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-4 aty)
% Number of variables : 69 ( 12 sgn 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,conjecture,
sdtasdt0(smndt0(xS),xR) = smndt0(xN),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f57_neg,negated_conjecture,
sdtasdt0(smndt0(xS),xR) != smndt0(xN),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f57_nnf,plain,
sdtasdt0(smndt0(xS),xR) != smndt0(xN),
inference(nnf_transformation,[status(thm)],[f57_neg]) ).
fof(f57_sk,plain,
sdtasdt0(smndt0(xS),xR) != smndt0(xN),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c91,plain,
sdtasdt0(smndt0(xS),xR) != smndt0(xN),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t172,plain,
eq(sdtasdt0(smndt0(xS),xR),smndt0(xN)) = false,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t5159,plain,
eq(sdtasdt0(smndt0(xS),xR),smndt0(xN)) = false,
inference(orient,[status(thm)],[t172]) ).
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/sandbox/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(c30,plain,
( sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t235,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,sdtasdt0(smndt0(X1),X2),smndt0(sdtasdt0(X1,X2))),smndt0(sdtasdt0(X1,X2))) = smndt0(sdtasdt0(X1,X2)),
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t3112,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,sdtasdt0(smndt0(X1),X2),smndt0(sdtasdt0(X1,X2))),smndt0(sdtasdt0(X1,X2))) = smndt0(sdtasdt0(X1,X2)),
inference(orient,[status(thm)],[t235]) ).
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/sandbox/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(t237,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,ifeq(aScalar0(X3),true,sdtasdt0(X1,X2),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)) = sdtasdt0(X2,X1),
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t2091,plain,
ifeq(aScalar0(X1),true,ifeq(aScalar0(X2),true,ifeq(aScalar0(X3),true,sdtasdt0(X1,X2),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)),sdtasdt0(X2,X1)) = sdtasdt0(X2,X1),
inference(orient,[status(thm)],[t237]) ).
fof(f54,hypothesis,
( xN = sdtasdt0(xR,xS)
& aScalar0(xN) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1949) ).
fof(f54_nnf,plain,
( xN = sdtasdt0(xR,xS)
& aScalar0(xN) ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
( xN = sdtasdt0(xR,xS)
& aScalar0(xN) ),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c88,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(t79,plain,
sdtasdt0(xR,xS) = xN,
inference(equality_encoding,[status(esa)],[c88]) ).
cnf(t2712,plain,
sdtasdt0(xR,xS) = xN,
inference(orient,[status(thm)],[t79]) ).
cnf(t2716,plain,
sdtasdt0(xR,xS) = ifeq(aScalar0(xS),true,ifeq(aScalar0(xR),true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),sdtasdt0(xR,xS)),
inference(cp,[status(thm)],[t2091,t2712]) ).
cnf(t13505,plain,
xN = ifeq(aScalar0(xS),true,ifeq(aScalar0(xR),true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t2716,t2712]) ).
fof(f53,hypothesis,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1930) ).
fof(f53_nnf,plain,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c85,plain,
aScalar0(xS),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(t13,plain,
aScalar0(xS) = true,
inference(equality_encoding,[status(esa)],[c85]) ).
cnf(t1284,plain,
aScalar0(xS) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t13506,plain,
xN = ifeq(true,true,ifeq(aScalar0(xR),true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t13505,t1284]) ).
cnf(t151,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t151]) ).
cnf(t13507,plain,
xN = ifeq(aScalar0(xR),true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t13506,t256]) ).
fof(f51,hypothesis,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1892) ).
fof(f51_nnf,plain,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c81,plain,
aScalar0(xR),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t12,plain,
aScalar0(xR) = true,
inference(equality_encoding,[status(esa)],[c81]) ).
cnf(t1253,plain,
aScalar0(xR) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t13508,plain,
xN = ifeq(true,true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t13507,t1253]) ).
cnf(t13509,plain,
xN = ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),
inference(step,[status(thm)],[t13508,t256]) ).
cnf(t12595,plain,
ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN) = xN,
inference(orient,[status(thm)],[t13509]) ).
fof(f11,axiom,
! [W0] :
( aScalar0(W0)
=> aScalar0(smndt0(W0)) ),
file('/export/starexec/sandbox/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(t182,plain,
ifeq(aScalar0(X1),true,aScalar0(smndt0(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t277,plain,
ifeq(aScalar0(X1),true,aScalar0(smndt0(X1)),true) = true,
inference(orient,[status(thm)],[t182]) ).
fof(f33,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( aDimensionOf0(W0) = aDimensionOf0(W1)
=> aScalar0(sdtasasdt0(W0,W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScPr) ).
fof(f33_nnf,plain,
! [W0,W1] :
( aScalar0(sdtasasdt0(W0,W1))
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [W0,W1] :
( aScalar0(sdtasasdt0(W0,W1))
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c52,plain,
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t230,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X2),true,ifeq(aDimensionOf0(X1),aDimensionOf0(X2),aScalar0(sdtasasdt0(X1,X2)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t289,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X2),true,ifeq(aDimensionOf0(X1),aDimensionOf0(X2),aScalar0(sdtasasdt0(X1,X2)),true),true),true) = true,
inference(orient,[status(thm)],[t230]) ).
cnf(t290,plain,
true = ifeq(aVector0(X1),true,ifeq(aVector0(X1),true,aScalar0(sdtasasdt0(X1,X1)),true),true),
inference(cp,[status(thm)],[t289,t256]) ).
cnf(t10869,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X1),true,aScalar0(sdtasasdt0(X1,X1)),true),true) = true,
inference(orient,[status(thm)],[t290]) ).
fof(f37,hypothesis,
( aVector0(xt)
& aVector0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678) ).
fof(f37_nnf,plain,
( aVector0(xt)
& aVector0(xs) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( aVector0(xt)
& aVector0(xs) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c57,plain,
aVector0(xt),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t17,plain,
aVector0(xt) = true,
inference(equality_encoding,[status(esa)],[c57]) ).
cnf(t1925,plain,
aVector0(xt) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t10870,plain,
true = ifeq(true,true,ifeq(aVector0(xt),true,aScalar0(sdtasasdt0(xt,xt)),true),true),
inference(cp,[status(thm)],[t10869,t1925]) ).
cnf(t13299,plain,
true = ifeq(aVector0(xt),true,aScalar0(sdtasasdt0(xt,xt)),true),
inference(step,[status(thm)],[t10870,t256]) ).
cnf(t13300,plain,
true = ifeq(true,true,aScalar0(sdtasasdt0(xt,xt)),true),
inference(step,[status(thm)],[t13299,t1925]) ).
cnf(t13301,plain,
true = aScalar0(sdtasasdt0(xt,xt)),
inference(step,[status(thm)],[t13300,t256]) ).
cnf(t10874,plain,
aScalar0(sdtasasdt0(xt,xt)) = true,
inference(orient,[status(thm)],[t13301]) ).
cnf(t10884,plain,
true = ifeq(true,true,aScalar0(smndt0(sdtasasdt0(xt,xt))),true),
inference(cp,[status(thm)],[t277,t10874]) ).
cnf(t13307,plain,
true = aScalar0(smndt0(sdtasasdt0(xt,xt))),
inference(step,[status(thm)],[t10884,t256]) ).
cnf(t11084,plain,
aScalar0(smndt0(sdtasasdt0(xt,xt))) = true,
inference(orient,[status(thm)],[t13307]) ).
cnf(t12596,plain,
xN = ifeq(true,true,sdtasdt0(xS,xR),xN),
inference(cp,[status(thm)],[t12595,t11084]) ).
cnf(t13510,plain,
xN = sdtasdt0(xS,xR),
inference(step,[status(thm)],[t12596,t256]) ).
cnf(t12639,plain,
sdtasdt0(xS,xR) = xN,
inference(orient,[status(thm)],[t13510]) ).
cnf(t12640,plain,
smndt0(sdtasdt0(xS,xR)) = ifeq(aScalar0(xS),true,ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),smndt0(sdtasdt0(xS,xR))),
inference(cp,[status(thm)],[t3112,t12639]) ).
cnf(t13511,plain,
smndt0(xN) = ifeq(aScalar0(xS),true,ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),smndt0(sdtasdt0(xS,xR))),
inference(step,[status(thm)],[t12640,t12639]) ).
cnf(t13512,plain,
smndt0(xN) = ifeq(true,true,ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),smndt0(sdtasdt0(xS,xR))),
inference(step,[status(thm)],[t13511,t1284]) ).
cnf(t13513,plain,
smndt0(xN) = ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),
inference(step,[status(thm)],[t13512,t256]) ).
cnf(t13514,plain,
smndt0(xN) = ifeq(true,true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),
inference(step,[status(thm)],[t13513,t1253]) ).
cnf(t13515,plain,
smndt0(xN) = sdtasdt0(smndt0(xS),xR),
inference(step,[status(thm)],[t13514,t256]) ).
cnf(t12681,plain,
sdtasdt0(smndt0(xS),xR) = smndt0(xN),
inference(orient,[status(thm)],[t13515]) ).
cnf(t13516,plain,
eq(smndt0(xN),smndt0(xN)) = false,
inference(step,[status(thm)],[t5159,t12681]) ).
cnf(t42,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1528,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(t13517,plain,
true = false,
inference(step,[status(thm)],[t13516,t1528]) ).
cnf(t12725,plain,
true = false,
inference(rw,[status(thm)],[t13517]) ).
cnf(t12727,plain,
false = true,
inference(orient,[status(thm)],[t12725]) ).
fof(f2,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) ) ),
file('/export/starexec/sandbox/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]) ).
fof(f40,hypothesis,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1692) ).
fof(f40_nnf,plain,
aDimensionOf0(xs) != sz00,
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
aDimensionOf0(xs) != sz00,
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c60,plain,
aDimensionOf0(xs) != sz00,
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c3,c60,c91]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t12727]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG059+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/5.44 % Computer : n008.cluster.edu
% 0.18/5.44 % Model : x86_64 x86_64
% 0.18/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.44 % Memory : 8046.5625MB
% 0.18/5.44 % OS : Linux 6.8.0-71-generic
% 0.18/5.44 % CPULimit : 300
% 0.18/5.44 % WCLimit : 300
% 0.18/5.44 % DateTime : Thu Sep 24 08:02:00 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.18/5.45 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 47.24/11.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.24/11.44 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------