%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG083+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 : 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:40 PM UTC 2026
% Result : Theorem 24.60s 3.92s
% Output : Proof 24.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 13
% Syntax : Number of formulae : 151 ( 113 unt; 0 def)
% Number of atoms : 225 ( 150 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 126 ( 52 ~; 46 |; 20 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 88 ( 2 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,conjecture,
( sz00 = sdtasdt0(sz00,xx)
& sdtasdt0(xx,sz00) = sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f16_neg,negated_conjecture,
~ ( sz00 = sdtasdt0(sz00,xx)
& sdtasdt0(xx,sz00) = sz00 ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
( sz00 != sdtasdt0(sz00,xx)
| sdtasdt0(xx,sz00) != sz00 ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( sz00 != sdtasdt0(sz00,xx)
| sdtasdt0(xx,sz00) != sz00 ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c21,plain,
( sz00 != sdtasdt0(sz00,xx)
| sdtasdt0(xx,sz00) != sz00 ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t247,plain,
ifeq(sdtasdt0(xx,sz00),sz00,ifeq(sz00,sdtasdt0(sz00,xx),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
fof(f10,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(f10_nnf,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c12,plain,
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi11,axiom,
ifeq(aElement0(X0),true,ifeq(aElement0(X1),true,sdtasdt0(X0,X1),sdtasdt0(X1,X0)),sdtasdt0(X1,X0)) = sdtasdt0(X1,X0),
inference(equality_encoding,[status(esa)],[c12]) ).
fof(f1,axiom,
aElement0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC) ).
fof(f1_nnf,plain,
aElement0(sz00),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
aElement0(sz00),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(hi0,axiom,
aElement0(sz00) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
fof(f15,hypothesis,
aElement0(xx),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__468) ).
fof(f15_nnf,plain,
aElement0(xx),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c20,plain,
aElement0(xx),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(hi19,axiom,
aElement0(xx) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t78,plain,
sdtasdt0(xx,sz00) = sdtasdt0(sz00,xx),
inference(hyper_resolution,[status(thm)],[hi11,hi0,hi19]) ).
cnf(t663,plain,
sdtasdt0(sz00,xx) = sdtasdt0(xx,sz00),
inference(orient,[status(thm)],[t78]) ).
cnf(t4120,plain,
ifeq(sdtasdt0(xx,sz00),sz00,ifeq(sz00,sdtasdt0(xx,sz00),false,true),true) = true,
inference(step,[status(thm)],[t247,t663]) ).
cnf(t2185,plain,
ifeq(sdtasdt0(xx,sz00),sz00,ifeq(sz00,sdtasdt0(xx,sz00),false,true),true) = true,
inference(orient,[status(thm)],[t4120]) ).
fof(f13,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ( sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAMDistr) ).
fof(f13_nnf,plain,
! [W0,W1,W2] :
( ( sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) )
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [W0,W1,W2] :
( ( sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) )
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c16,plain,
( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t254,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,sdtasdt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t1500,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,sdtasdt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)),
inference(orient,[status(thm)],[t254]) ).
fof(f9,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddInvr) ).
fof(f9_nnf,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c10,plain,
( sdtpldt0(X0,smndt0(X0)) = sz00
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t198,plain,
ifeq(aElement0(X1),true,sdtpldt0(X1,smndt0(X1)),sz00) = sz00,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t306,plain,
ifeq(aElement0(X1),true,sdtpldt0(X1,smndt0(X1)),sz00) = sz00,
inference(orient,[status(thm)],[t198]) ).
fof(f5,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f5_nnf,plain,
! [W0,W1] :
( aElement0(sdtasdt0(W0,W1))
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [W0,W1] :
( aElement0(sdtasdt0(W0,W1))
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi4,axiom,
ifeq(aElement0(X0),true,ifeq(aElement0(X1),true,aElement0(sdtasdt0(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t18,plain,
aElement0(sdtasdt0(sz00,xx)) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi0,hi19]) ).
cnf(t4115,plain,
aElement0(sdtasdt0(xx,sz00)) = true,
inference(step,[status(thm)],[t18,t663]) ).
cnf(t1994,plain,
aElement0(sdtasdt0(xx,sz00)) = true,
inference(orient,[status(thm)],[t4115]) ).
cnf(t2000,plain,
sz00 = ifeq(true,true,sdtpldt0(sdtasdt0(xx,sz00),smndt0(sdtasdt0(xx,sz00))),sz00),
inference(cp,[status(thm)],[t306,t1994]) ).
cnf(t66,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t66]) ).
cnf(t4265,plain,
sz00 = sdtpldt0(sdtasdt0(xx,sz00),smndt0(sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t2000,t256]) ).
fof(f11,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
fof(f11_nnf,plain,
! [W0,W1,W2] :
( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [W0,W1,W2] :
( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c13,plain,
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t252,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,sdtasdt0(sdtasdt0(X1,X2),X3),sdtasdt0(X1,sdtasdt0(X2,X3))),sdtasdt0(X1,sdtasdt0(X2,X3))),sdtasdt0(X1,sdtasdt0(X2,X3))) = sdtasdt0(X1,sdtasdt0(X2,X3)),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t497,plain,
ifeq(aElement0(X1),true,ifeq(aElement0(X2),true,ifeq(aElement0(X3),true,sdtasdt0(sdtasdt0(X1,X2),X3),sdtasdt0(X1,sdtasdt0(X2,X3))),sdtasdt0(X1,sdtasdt0(X2,X3))),sdtasdt0(X1,sdtasdt0(X2,X3))) = sdtasdt0(X1,sdtasdt0(X2,X3)),
inference(orient,[status(thm)],[t252]) ).
fof(f14,axiom,
! [W0] :
( aElement0(W0)
=> ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulMnOne) ).
fof(f14_nnf,plain,
! [W0] :
( ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) )
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [W0] :
( ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) )
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c18,plain,
( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t240,plain,
ifeq(aElement0(X1),true,sdtasdt0(smndt0(sz10),X1),smndt0(X1)) = smndt0(X1),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t313,plain,
ifeq(aElement0(X1),true,sdtasdt0(smndt0(sz10),X1),smndt0(X1)) = smndt0(X1),
inference(orient,[status(thm)],[t240]) ).
cnf(t1995,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(true,true,sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00)),smndt0(sdtasdt0(xx,sz00))),
inference(cp,[status(thm)],[t313,t1994]) ).
cnf(t4203,plain,
smndt0(sdtasdt0(xx,sz00)) = sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00)),
inference(step,[status(thm)],[t1995,t256]) ).
cnf(t3540,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00)) = smndt0(sdtasdt0(xx,sz00)),
inference(orient,[status(thm)],[t4203]) ).
cnf(t3542,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00)) = ifeq(aElement0(smndt0(sz10)),true,ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),
inference(cp,[status(thm)],[t497,t3540]) ).
cnf(t4204,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(aElement0(smndt0(sz10)),true,ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t3542,t3540]) ).
fof(f3,axiom,
! [W0] :
( aElement0(W0)
=> aElement0(smndt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsU) ).
fof(f3_nnf,plain,
! [W0] :
( aElement0(smndt0(W0))
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [W0] :
( aElement0(smndt0(W0))
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi2,axiom,
ifeq(aElement0(X0),true,aElement0(smndt0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
fof(f2,axiom,
aElement0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f2_nnf,plain,
aElement0(sz10),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
aElement0(sz10),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(hi1,axiom,
aElement0(sz10) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t4,plain,
aElement0(smndt0(sz10)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi1]) ).
cnf(t1891,plain,
aElement0(smndt0(sz10)) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t4205,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(true,true,ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4204,t1891]) ).
cnf(t4206,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4205,t256]) ).
cnf(t2,plain,
aElement0(xx) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t1933,plain,
aElement0(xx) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t4207,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(true,true,ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),sdtasdt0(smndt0(sz10),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4206,t1933]) ).
cnf(t4208,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(aElement0(sz00),true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4207,t256]) ).
cnf(t0,plain,
aElement0(sz00) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t1792,plain,
aElement0(sz00) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t4209,plain,
smndt0(sdtasdt0(xx,sz00)) = ifeq(true,true,sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),smndt0(sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4208,t1792]) ).
cnf(t4210,plain,
smndt0(sdtasdt0(xx,sz00)) = sdtasdt0(sdtasdt0(smndt0(sz10),xx),sz00),
inference(step,[status(thm)],[t4209,t256]) ).
cnf(hi17,axiom,
ifeq(aElement0(X0),true,sdtasdt0(smndt0(sz10),X0),smndt0(X0)) = smndt0(X0),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t70,plain,
sdtasdt0(smndt0(sz10),xx) = smndt0(xx),
inference(hyper_resolution,[status(thm)],[hi17,hi19]) ).
cnf(t343,plain,
sdtasdt0(smndt0(sz10),xx) = smndt0(xx),
inference(orient,[status(thm)],[t70]) ).
cnf(t4211,plain,
smndt0(sdtasdt0(xx,sz00)) = sdtasdt0(smndt0(xx),sz00),
inference(step,[status(thm)],[t4210,t343]) ).
cnf(h156,plain,
aElement0(smndt0(xx)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi19]) ).
cnf(t114,plain,
sdtasdt0(sz00,smndt0(xx)) = sdtasdt0(smndt0(xx),sz00),
inference(hyper_resolution,[status(thm)],[hi11,hi0,h156]) ).
cnf(t655,plain,
sdtasdt0(smndt0(xx),sz00) = sdtasdt0(sz00,smndt0(xx)),
inference(orient,[status(thm)],[t114]) ).
cnf(t4212,plain,
smndt0(sdtasdt0(xx,sz00)) = sdtasdt0(sz00,smndt0(xx)),
inference(step,[status(thm)],[t4211,t655]) ).
cnf(t3560,plain,
smndt0(sdtasdt0(xx,sz00)) = sdtasdt0(sz00,smndt0(xx)),
inference(orient,[status(thm)],[t4212]) ).
cnf(t4266,plain,
sz00 = sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(sz00,smndt0(xx))),
inference(step,[status(thm)],[t4265,t3560]) ).
cnf(t4024,plain,
sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(sz00,smndt0(xx))) = sz00,
inference(orient,[status(thm)],[t4266]) ).
cnf(h150,plain,
aElement0(sdtasdt0(xx,sz00)) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi19,hi0]) ).
cnf(c19,plain,
( smndt0(X0) = sdtasdt0(X0,smndt0(sz10))
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi18,axiom,
ifeq(aElement0(X0),true,smndt0(X0),sdtasdt0(X0,smndt0(sz10))) = sdtasdt0(X0,smndt0(sz10)),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t205,plain,
sdtasdt0(sdtasdt0(xx,sz00),smndt0(sz10)) = smndt0(sdtasdt0(xx,sz00)),
inference(hyper_resolution,[status(thm)],[hi18,h150]) ).
cnf(t354,plain,
sdtasdt0(sdtasdt0(xx,sz00),smndt0(sz10)) = smndt0(sdtasdt0(xx,sz00)),
inference(orient,[status(thm)],[t205]) ).
cnf(t499,plain,
sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10))) = ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(cp,[status(thm)],[t497,t354]) ).
cnf(t72,plain,
sdtasdt0(sz00,smndt0(sz10)) = smndt0(sz00),
inference(hyper_resolution,[status(thm)],[hi18,hi0]) ).
cnf(t314,plain,
sdtasdt0(sz00,smndt0(sz10)) = smndt0(sz00),
inference(orient,[status(thm)],[t72]) ).
cnf(h13,plain,
aElement0(smndt0(sz00)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi0]) ).
fof(f8,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(f8_nnf,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c9,plain,
( X0 = sdtpldt0(sz00,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(aElement0(X0),true,X0,sdtpldt0(sz00,X0)) = sdtpldt0(sz00,X0),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t83,plain,
sdtpldt0(sz00,smndt0(sz00)) = smndt0(sz00),
inference(hyper_resolution,[status(thm)],[hi8,h13]) ).
cnf(hi9,axiom,
ifeq(aElement0(X0),true,sdtpldt0(X0,smndt0(X0)),sz00) = sz00,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t40,plain,
sdtpldt0(sz00,smndt0(sz00)) = sz00,
inference(hyper_resolution,[status(thm)],[hi9,hi0]) ).
cnf(t264,plain,
sdtpldt0(sz00,smndt0(sz00)) = sz00,
inference(orient,[status(thm)],[t40]) ).
cnf(t4098,plain,
sz00 = smndt0(sz00),
inference(step,[status(thm)],[t83,t264]) ).
cnf(t320,plain,
smndt0(sz00) = sz00,
inference(orient,[status(thm)],[t4098]) ).
cnf(t4099,plain,
sdtasdt0(sz00,smndt0(sz10)) = sz00,
inference(step,[status(thm)],[t314,t320]) ).
cnf(t321,plain,
sdtasdt0(sz00,smndt0(sz10)) = sz00,
inference(orient,[status(thm)],[t4099]) ).
cnf(t4267,plain,
sdtasdt0(xx,sz00) = ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t499,t321]) ).
cnf(t4268,plain,
sdtasdt0(xx,sz00) = ifeq(true,true,ifeq(aElement0(sz00),true,ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t4267,t1933]) ).
cnf(t4269,plain,
sdtasdt0(xx,sz00) = ifeq(aElement0(sz00),true,ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t4268,t256]) ).
cnf(t4270,plain,
sdtasdt0(xx,sz00) = ifeq(true,true,ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t4269,t1792]) ).
cnf(t4271,plain,
sdtasdt0(xx,sz00) = ifeq(aElement0(smndt0(sz10)),true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t4270,t256]) ).
cnf(t4272,plain,
sdtasdt0(xx,sz00) = ifeq(true,true,smndt0(sdtasdt0(xx,sz00)),sdtasdt0(xx,sdtasdt0(sz00,smndt0(sz10)))),
inference(step,[status(thm)],[t4271,t1891]) ).
cnf(t4273,plain,
sdtasdt0(xx,sz00) = smndt0(sdtasdt0(xx,sz00)),
inference(step,[status(thm)],[t4272,t256]) ).
cnf(t4274,plain,
sdtasdt0(xx,sz00) = sdtasdt0(sz00,smndt0(xx)),
inference(step,[status(thm)],[t4273,t3560]) ).
cnf(t4034,plain,
sdtasdt0(sz00,smndt0(xx)) = sdtasdt0(xx,sz00),
inference(orient,[status(thm)],[t4274]) ).
cnf(t4283,plain,
sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00)) = sz00,
inference(step,[status(thm)],[t4024,t4034]) ).
cnf(t4059,plain,
sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00)) = sz00,
inference(rw,[status(thm)],[t4283]) ).
cnf(t4060,plain,
sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00)) = sz00,
inference(orient,[status(thm)],[t4059]) ).
cnf(t4062,plain,
sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00)) = ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),
inference(cp,[status(thm)],[t1500,t4060]) ).
cnf(t4284,plain,
sz00 = ifeq(aElement0(xx),true,ifeq(aElement0(sz00),true,ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4062,t4060]) ).
cnf(t4285,plain,
sz00 = ifeq(true,true,ifeq(aElement0(sz00),true,ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4284,t1933]) ).
cnf(t4286,plain,
sz00 = ifeq(aElement0(sz00),true,ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4285,t256]) ).
cnf(t4287,plain,
sz00 = ifeq(true,true,ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),sdtpldt0(sdtasdt0(xx,sz00),sdtasdt0(xx,sz00))),
inference(step,[status(thm)],[t4286,t1792]) ).
cnf(t4288,plain,
sz00 = ifeq(aElement0(sz00),true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),
inference(step,[status(thm)],[t4287,t256]) ).
cnf(t4289,plain,
sz00 = ifeq(true,true,sdtasdt0(xx,sdtpldt0(sz00,sz00)),sz00),
inference(step,[status(thm)],[t4288,t1792]) ).
cnf(t4290,plain,
sz00 = sdtasdt0(xx,sdtpldt0(sz00,sz00)),
inference(step,[status(thm)],[t4289,t256]) ).
cnf(t11,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(hyper_resolution,[status(thm)],[hi8,hi0]) ).
cnf(t262,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(orient,[status(thm)],[t11]) ).
cnf(t4291,plain,
sz00 = sdtasdt0(xx,sz00),
inference(step,[status(thm)],[t4290,t262]) ).
cnf(t4073,plain,
sdtasdt0(xx,sz00) = sz00,
inference(orient,[status(thm)],[t4291]) ).
cnf(t4298,plain,
ifeq(sz00,sz00,ifeq(sz00,sdtasdt0(xx,sz00),false,true),true) = true,
inference(step,[status(thm)],[t2185,t4073]) ).
cnf(t4299,plain,
ifeq(sz00,sdtasdt0(xx,sz00),false,true) = true,
inference(step,[status(thm)],[t4298,t256]) ).
cnf(t4300,plain,
ifeq(sz00,sz00,false,true) = true,
inference(step,[status(thm)],[t4299,t4073]) ).
cnf(t4301,plain,
false = true,
inference(step,[status(thm)],[t4300,t256]) ).
cnf(t4096,plain,
false = true,
inference(rw,[status(thm)],[t4301]) ).
cnf(t4097,plain,
false = true,
inference(orient,[status(thm)],[t4096]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4097]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG083+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 08:08:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 24.60/3.92 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.60/3.92 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------