%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG059+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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 60.44s 8.16s
% Output : Proof 60.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 21
% Syntax : Number of formulae : 164 ( 116 unt; 0 def)
% Number of atoms : 268 ( 179 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 160 ( 56 ~; 44 |; 51 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 14 con; 0-4 aty)
% Number of variables : 92 ( 12 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,conjecture,
sdtasdt0(smndt0(xS),xR) = smndt0(xN),
file('/export/starexec/sandbox2/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(c95,plain,
sdtasdt0(smndt0(xS),xR) != smndt0(xN),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t163,plain,
eq(sdtasdt0(smndt0(xS),xR),smndt0(xN)) = false,
inference(equality_encoding,[status(esa)],[c95]) ).
cnf(t4966,plain,
eq(sdtasdt0(smndt0(xS),xR),smndt0(xN)) = false,
inference(orient,[status(thm)],[t163]) ).
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(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(t2738,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/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(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(t2051,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/sandbox2/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(c92,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(t77,plain,
sdtasdt0(xR,xS) = xN,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t4116,plain,
sdtasdt0(xR,xS) = xN,
inference(orient,[status(thm)],[t77]) ).
cnf(t4124,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)],[t2051,t4116]) ).
cnf(t18940,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)],[t4124,t4116]) ).
fof(f53,hypothesis,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
file('/export/starexec/sandbox2/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(c89,plain,
aScalar0(xS),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(t13,plain,
aScalar0(xS) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(t1340,plain,
aScalar0(xS) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t18941,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)],[t18940,t1340]) ).
cnf(t144,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t144]) ).
cnf(t18942,plain,
xN = ifeq(aScalar0(xR),true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t18941,t256]) ).
fof(f51,hypothesis,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
file('/export/starexec/sandbox2/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(c85,plain,
aScalar0(xR),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t12,plain,
aScalar0(xR) = true,
inference(equality_encoding,[status(esa)],[c85]) ).
cnf(t1185,plain,
aScalar0(xR) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t18943,plain,
xN = ifeq(true,true,ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),sdtasdt0(xR,xS)),
inference(step,[status(thm)],[t18942,t1185]) ).
cnf(t18944,plain,
xN = ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN),
inference(step,[status(thm)],[t18943,t256]) ).
cnf(t17718,plain,
ifeq(aScalar0(X1),true,sdtasdt0(xS,xR),xN) = xN,
inference(orient,[status(thm)],[t18944]) ).
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(t183,plain,
ifeq(aScalar0(X1),true,aScalar0(smndt0(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t278,plain,
ifeq(aScalar0(X1),true,aScalar0(smndt0(X1)),true) = true,
inference(orient,[status(thm)],[t183]) ).
fof(f33,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( aDimensionOf0(W0) = aDimensionOf0(W1)
=> aScalar0(sdtasasdt0(W0,W1)) ) ),
file('/export/starexec/sandbox2/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(t12271,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/sandbox2/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(t1728,plain,
aVector0(xt) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t12273,plain,
true = ifeq(true,true,ifeq(aVector0(xt),true,aScalar0(sdtasasdt0(xt,xt)),true),true),
inference(cp,[status(thm)],[t12271,t1728]) ).
cnf(t18427,plain,
true = ifeq(aVector0(xt),true,aScalar0(sdtasasdt0(xt,xt)),true),
inference(step,[status(thm)],[t12273,t256]) ).
cnf(t18428,plain,
true = ifeq(true,true,aScalar0(sdtasasdt0(xt,xt)),true),
inference(step,[status(thm)],[t18427,t1728]) ).
cnf(t18429,plain,
true = aScalar0(sdtasasdt0(xt,xt)),
inference(step,[status(thm)],[t18428,t256]) ).
cnf(t12340,plain,
aScalar0(sdtasasdt0(xt,xt)) = true,
inference(orient,[status(thm)],[t18429]) ).
cnf(t12350,plain,
true = ifeq(true,true,aScalar0(smndt0(sdtasasdt0(xt,xt))),true),
inference(cp,[status(thm)],[t278,t12340]) ).
cnf(t18435,plain,
true = aScalar0(smndt0(sdtasasdt0(xt,xt))),
inference(step,[status(thm)],[t12350,t256]) ).
cnf(t12634,plain,
aScalar0(smndt0(sdtasasdt0(xt,xt))) = true,
inference(orient,[status(thm)],[t18435]) ).
cnf(t165,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t263,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t165]) ).
fof(f35,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( ( aDimensionOf0(W1) != sz00
& aDimensionOf0(W0) = aDimensionOf0(W1) )
=> sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSPN) ).
fof(f35_nnf,plain,
! [W0,W1] :
( sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1))))
| aDimensionOf0(W1) = sz00
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [W0,W1] :
( sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1))))
| aDimensionOf0(W1) = sz00
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c54,plain,
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t251,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X2),true,ifeq(aDimensionOf0(X1),aDimensionOf0(X2),or(eq(aDimensionOf0(X2),sz00),eq(sdtasasdt0(X1,X2),sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X2)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X2,aDimensionOf0(X2)))))),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t293,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X2),true,ifeq(aDimensionOf0(X1),aDimensionOf0(X2),or(eq(aDimensionOf0(X2),sz00),eq(sdtasasdt0(X1,X2),sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X2)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X2,aDimensionOf0(X2)))))),true),true),true) = true,
inference(orient,[status(thm)],[t251]) ).
cnf(t294,plain,
true = ifeq(aVector0(X1),true,ifeq(aVector0(X1),true,or(eq(aDimensionOf0(X1),sz00),eq(sdtasasdt0(X1,X1),sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X1,aDimensionOf0(X1)))))),true),true),
inference(cp,[status(thm)],[t293,t256]) ).
cnf(t15122,plain,
ifeq(aVector0(X1),true,ifeq(aVector0(X1),true,or(eq(aDimensionOf0(X1),sz00),eq(sdtasasdt0(X1,X1),sdtpldt0(sdtasasdt0(sziznziztdt0(X1),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X1,aDimensionOf0(X1)),sdtlbdtrb0(X1,aDimensionOf0(X1)))))),true),true) = true,
inference(orient,[status(thm)],[t294]) ).
cnf(t15126,plain,
true = ifeq(true,true,ifeq(aVector0(xt),true,or(eq(aDimensionOf0(xt),sz00),eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),true),true),
inference(cp,[status(thm)],[t15122,t1728]) ).
cnf(t18733,plain,
true = ifeq(aVector0(xt),true,or(eq(aDimensionOf0(xt),sz00),eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),true),
inference(step,[status(thm)],[t15126,t256]) ).
cnf(t18734,plain,
true = ifeq(true,true,or(eq(aDimensionOf0(xt),sz00),eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),true),
inference(step,[status(thm)],[t18733,t1728]) ).
cnf(t18735,plain,
true = or(eq(aDimensionOf0(xt),sz00),eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),
inference(step,[status(thm)],[t18734,t256]) ).
fof(f40,hypothesis,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox2/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(t138,plain,
eq(aDimensionOf0(xs),sz00) = false,
inference(equality_encoding,[status(esa)],[c60]) ).
fof(f39,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1678_01) ).
fof(f39_nnf,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c59,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(t23,plain,
aDimensionOf0(xt) = aDimensionOf0(xs),
inference(equality_encoding,[status(esa)],[c59]) ).
cnf(t4398,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(orient,[status(thm)],[t23]) ).
cnf(t17930,plain,
eq(aDimensionOf0(xt),sz00) = false,
inference(step,[status(thm)],[t138,t4398]) ).
cnf(t4968,plain,
eq(aDimensionOf0(xt),sz00) = false,
inference(orient,[status(thm)],[t17930]) ).
cnf(t18736,plain,
true = or(false,eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt)))))),
inference(step,[status(thm)],[t18735,t4968]) ).
cnf(t45,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t267,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t45]) ).
cnf(t18737,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt))))),
inference(step,[status(thm)],[t18736,t267]) ).
fof(f42,hypothesis,
( xq = sziznziztdt0(xt)
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1726) ).
fof(f42_nnf,plain,
( xq = sziznziztdt0(xt)
& ! [W0] :
( sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [W0] :
( xq = sziznziztdt0(xt)
& ( sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c68,plain,
xq = sziznziztdt0(xt),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t22,plain,
sziznziztdt0(xt) = xq,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(t4982,plain,
sziznziztdt0(xt) = xq,
inference(orient,[status(thm)],[t22]) ).
cnf(t18738,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(xq,sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt))))),
inference(step,[status(thm)],[t18737,t4982]) ).
cnf(t18739,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(sdtasasdt0(xq,xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt))))),
inference(step,[status(thm)],[t18738,t4982]) ).
fof(f46,hypothesis,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1800) ).
fof(f46_nnf,plain,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c76,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(t49,plain,
sdtasasdt0(xq,xq) = xD,
inference(equality_encoding,[status(esa)],[c76]) ).
cnf(t5012,plain,
sdtasasdt0(xq,xq) = xD,
inference(orient,[status(thm)],[t49]) ).
cnf(t18740,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(xD,sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xt)),sdtlbdtrb0(xt,aDimensionOf0(xt))))),
inference(step,[status(thm)],[t18739,t5012]) ).
fof(f44,hypothesis,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1766) ).
fof(f44_nnf,plain,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c72,plain,
xB = sdtlbdtrb0(xt,aDimensionOf0(xt)),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(t141,plain,
sdtlbdtrb0(xt,aDimensionOf0(xt)) = xB,
inference(equality_encoding,[status(esa)],[c72]) ).
cnf(t4940,plain,
sdtlbdtrb0(xt,aDimensionOf0(xt)) = xB,
inference(orient,[status(thm)],[t141]) ).
cnf(t18741,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(xD,sdtasdt0(xB,sdtlbdtrb0(xt,aDimensionOf0(xt))))),
inference(step,[status(thm)],[t18740,t4940]) ).
cnf(t18742,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(xD,sdtasdt0(xB,xB))),
inference(step,[status(thm)],[t18741,t4940]) ).
fof(f49,hypothesis,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1854) ).
fof(f49_nnf,plain,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c82,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t65,plain,
sdtasdt0(xB,xB) = xG,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(t3790,plain,
sdtasdt0(xB,xB) = xG,
inference(orient,[status(thm)],[t65]) ).
cnf(t18743,plain,
true = eq(sdtasasdt0(xt,xt),sdtpldt0(xD,xG)),
inference(step,[status(thm)],[t18742,t3790]) ).
cnf(t15509,plain,
eq(sdtasasdt0(xt,xt),sdtpldt0(xD,xG)) = true,
inference(orient,[status(thm)],[t18743]) ).
cnf(t15510,plain,
sdtpldt0(xD,xG) = ifeq(true,true,sdtasasdt0(xt,xt),sdtpldt0(xD,xG)),
inference(cp,[status(thm)],[t263,t15509]) ).
cnf(t18744,plain,
sdtpldt0(xD,xG) = sdtasasdt0(xt,xt),
inference(step,[status(thm)],[t15510,t256]) ).
cnf(t15511,plain,
sdtasasdt0(xt,xt) = sdtpldt0(xD,xG),
inference(orient,[status(thm)],[t18744]) ).
cnf(t18759,plain,
aScalar0(smndt0(sdtpldt0(xD,xG))) = true,
inference(step,[status(thm)],[t12634,t15511]) ).
cnf(t15526,plain,
aScalar0(smndt0(sdtpldt0(xD,xG))) = true,
inference(rw,[status(thm)],[t18759]) ).
cnf(t15692,plain,
aScalar0(smndt0(sdtpldt0(xD,xG))) = true,
inference(orient,[status(thm)],[t15526]) ).
cnf(t17719,plain,
xN = ifeq(true,true,sdtasdt0(xS,xR),xN),
inference(cp,[status(thm)],[t17718,t15692]) ).
cnf(t18945,plain,
xN = sdtasdt0(xS,xR),
inference(step,[status(thm)],[t17719,t256]) ).
cnf(t17788,plain,
sdtasdt0(xS,xR) = xN,
inference(orient,[status(thm)],[t18945]) ).
cnf(t17791,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)],[t2738,t17788]) ).
cnf(t18946,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)],[t17791,t17788]) ).
cnf(t18947,plain,
smndt0(xN) = ifeq(true,true,ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),smndt0(sdtasdt0(xS,xR))),
inference(step,[status(thm)],[t18946,t1340]) ).
cnf(t18948,plain,
smndt0(xN) = ifeq(aScalar0(xR),true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),
inference(step,[status(thm)],[t18947,t256]) ).
cnf(t18949,plain,
smndt0(xN) = ifeq(true,true,sdtasdt0(smndt0(xS),xR),smndt0(xN)),
inference(step,[status(thm)],[t18948,t1185]) ).
cnf(t18950,plain,
smndt0(xN) = sdtasdt0(smndt0(xS),xR),
inference(step,[status(thm)],[t18949,t256]) ).
cnf(t17830,plain,
sdtasdt0(smndt0(xS),xR) = smndt0(xN),
inference(orient,[status(thm)],[t18950]) ).
cnf(t18951,plain,
eq(smndt0(xN),smndt0(xN)) = false,
inference(step,[status(thm)],[t4966,t17830]) ).
cnf(t42,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1429,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(t18952,plain,
true = false,
inference(step,[status(thm)],[t18951,t1429]) ).
cnf(t17874,plain,
true = false,
inference(rw,[status(thm)],[t18952]) ).
cnf(t17876,plain,
false = true,
inference(orient,[status(thm)],[t17874]) ).
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,c60,c95]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t17876]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG059+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 08:00:59 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 60.44/8.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.44/8.16 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------