%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG098+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 08:26:38 AM UTC 2026
% Result : Theorem 113.59s 15.74s
% Output : CNFRefutation 113.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 21
% Syntax : Number of formulae : 147 ( 84 unt; 0 def)
% Number of atoms : 273 ( 91 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 221 ( 95 ~; 85 |; 22 &)
% ( 3 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 110 ( 0 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsU,axiom,
! [W0] :
( aElement0(W0)
=> aElement0(smndt0(W0)) ),
file('theBenchmark.p',mSortsU) ).
fof(mSortsB_02,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mSortsB_02) ).
fof(mAddComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('theBenchmark.p',mAddComm) ).
fof(mAddAsso,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('theBenchmark.p',mAddAsso) ).
fof(mAddZero,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('theBenchmark.p',mAddZero) ).
fof(mAddInvr,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('theBenchmark.p',mAddInvr) ).
fof(mMulComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
fof(mMulAsso,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ),
file('theBenchmark.p',mMulAsso) ).
fof(mAMDistr,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('theBenchmark.p',mAMDistr) ).
fof(mMulMnOne,axiom,
! [W0] :
( aElement0(W0)
=> ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) ) ),
file('theBenchmark.p',mMulMnOne) ).
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefSInt,axiom,
! [W0,W1] :
( ( aSet0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtasasdt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
file('theBenchmark.p',mDefSInt) ).
fof(mDefIdeal,axiom,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( aElementOf0(W1,W0)
=> ( ! [W2] :
( aElement0(W2)
=> aElementOf0(sdtasdt0(W2,W1),W0) )
& ! [W2] :
( aElementOf0(W2,W0)
=> aElementOf0(sdtpldt0(W1,W2),W0) ) ) )
& aSet0(W0) ) ),
file('theBenchmark.p',mDefIdeal) ).
fof(m__1205,axiom,
( aIdeal0(xJ)
& aIdeal0(xI) ),
file('theBenchmark.p',m__1205) ).
fof(m__1217,axiom,
( aElement0(xy)
& aElement0(xx) ),
file('theBenchmark.p',m__1217) ).
fof(m__1294,axiom,
( sdtpldt0(xa,xb) = sz10
& aElementOf0(xb,xJ)
& aElementOf0(xa,xI) ),
file('theBenchmark.p',m__1294) ).
fof(m__,conjecture,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_32,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(clausify,[status(thm)],[m___neg]) ).
fof(m__1393,axiom,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
file('theBenchmark.p',m__1393) ).
cnf(c_33,plain,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
inference(clausify,[status(thm)],[m__1393]) ).
fof(m__1374,axiom,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
file('theBenchmark.p',m__1374) ).
cnf(c_34,plain,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
inference(clausify,[status(thm)],[m__1374]) ).
cnf(c_35,plain,
sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))) = sdtpldt0(xw,smndt0(xx)),
inference(copy,[status(thm)],[c_34]) ).
fof(m__1319,axiom,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
file('theBenchmark.p',m__1319) ).
cnf(c_36,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(clausify,[status(thm)],[m__1319]) ).
cnf(c_37,plain,
sdtpldt0(xa,xb) = sz10,
inference(clausify,[status(thm)],[m__1294]) ).
cnf(c_38,plain,
sz10 = sdtpldt0(xa,xb),
inference(copy,[status(thm)],[c_37]) ).
cnf(c_39,plain,
aElementOf0(xb,xJ),
inference(clausify,[status(thm)],[m__1294]) ).
cnf(c_40,plain,
aElementOf0(xa,xI),
inference(clausify,[status(thm)],[m__1294]) ).
cnf(c_41,plain,
aElement0(xy),
inference(clausify,[status(thm)],[m__1217]) ).
cnf(c_42,plain,
aElement0(xx),
inference(clausify,[status(thm)],[m__1217]) ).
cnf(c_44,plain,
aIdeal0(xJ),
inference(clausify,[status(thm)],[m__1205]) ).
cnf(c_45,plain,
aIdeal0(xI),
inference(clausify,[status(thm)],[m__1205]) ).
cnf(c_53,plain,
( aElementOf0(sdtasdt0(C,B),A)
| ~ aElement0(C)
| ~ aElementOf0(B,A)
| ~ aIdeal0(A) ),
inference(clausify,[status(thm)],[mDefIdeal]) ).
cnf(c_54,plain,
( aElementOf0(sdtpldt0(B,C),A)
| ~ aElementOf0(C,A)
| ~ aElementOf0(B,A)
| ~ aIdeal0(A) ),
inference(clausify,[status(thm)],[mDefIdeal]) ).
cnf(c_55,plain,
( aSet0(A)
| ~ aIdeal0(A) ),
inference(clausify,[status(thm)],[mDefIdeal]) ).
cnf(c_59,plain,
( ~ aElementOf0(D,B)
| ~ aElementOf0(D,A)
| aElementOf0(D,C)
| sdtasasdt0(A,B) != C
| ~ aSet0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSInt]) ).
cnf(c_60,plain,
( aElementOf0(D,B)
| ~ aElementOf0(D,C)
| sdtasasdt0(A,B) != C
| ~ aSet0(B)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mDefSInt]) ).
cnf(c_77,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_84,plain,
( sdtasdt0(A,smndt0(sz10)) = smndt0(A)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulMnOne]) ).
cnf(c_85,plain,
( sdtasdt0(A,smndt0(sdtpldt0(xa,xb))) = smndt0(A)
| ~ aElement0(A) ),
inference(paramod,[status(thm)],[c_38,c_84]) ).
cnf(c_90,plain,
( sdtasdt0(A,sdtpldt0(B,C)) = sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAMDistr]) ).
cnf(c_91,plain,
( sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C)) = sdtasdt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_90]) ).
cnf(c_96,plain,
( sdtasdt0(sdtasdt0(A,B),C) = sdtasdt0(A,sdtasdt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulAsso]) ).
cnf(c_97,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_99,plain,
( sdtpldt0(A,smndt0(A)) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddInvr]) ).
cnf(c_101,plain,
( sdtpldt0(A,sz00) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_102,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_103,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddComm]) ).
cnf(c_104,plain,
( aElement0(sdtasdt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_106,plain,
( aElement0(smndt0(A))
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mSortsU]) ).
fof(mSortsC_01,axiom,
aElement0(sz10),
file('theBenchmark.p',mSortsC_01) ).
cnf(c_107,plain,
aElement0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
cnf(c_108,plain,
aElement0(sdtpldt0(xa,xb)),
inference(paramod,[status(thm)],[c_38,c_107]) ).
cnf(c_20947,plain,
sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))) = sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xx)),
inference(paramod,[status(thm)],[c_36,c_35]) ).
cnf(c_110,plain,
sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
inference(copy,[status(thm)],[c_20947]) ).
cnf(c_20948,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xx)),xI),
inference(paramod,[status(thm)],[c_36,c_32]) ).
cnf(c_111,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),xI),
inference(paramod,[status(thm)],[c_110,c_20948]) ).
cnf(c_112,plain,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),xI),
inference(paramod,[status(thm)],[c_38,c_33]) ).
cnf(c_20949,plain,
( ~ aElementOf0(C,A)
| ~ aElementOf0(C,A)
| aElementOf0(C,B)
| sdtasasdt0(A,A) != B
| ~ aSet0(A) ),
inference(factor,[status(thm)],[c_59]) ).
cnf(c_123,plain,
( ~ aElementOf0(C,A)
| aElementOf0(C,B)
| sdtasasdt0(A,A) != B
| ~ aSet0(A) ),
inference(copy,[status(thm)],[c_20949]) ).
cnf(c_124,plain,
( aElementOf0(C,A)
| ~ aElementOf0(C,B)
| sdtasasdt0(A,A) != B
| ~ aSet0(A) ),
inference(factor,[status(thm)],[c_60]) ).
cnf(c_20950,plain,
( aElementOf0(sdtasdt0(B,A),xI)
| ~ aElement0(B)
| ~ aElementOf0(A,xI) ),
inference(resolve,[status(thm)],[c_53,c_45]) ).
cnf(c_20951,plain,
( aElementOf0(sdtasdt0(A,xa),xI)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20950,c_40]) ).
cnf(c_197,plain,
aElementOf0(sdtasdt0(xy,xa),xI),
inference(resolve,[status(thm)],[c_20951,c_41]) ).
cnf(c_206,plain,
aSet0(xI),
inference(resolve,[status(thm)],[c_55,c_45]) ).
cnf(c_207,plain,
aSet0(xJ),
inference(resolve,[status(thm)],[c_55,c_44]) ).
cnf(c_20952,plain,
( aElement0(xa)
| ~ aSet0(xI) ),
inference(resolve,[status(thm)],[c_77,c_40]) ).
cnf(c_246,plain,
aElement0(xa),
inference(resolve,[status(thm)],[c_206,c_20952]) ).
cnf(c_20953,plain,
( aElement0(xb)
| ~ aSet0(xJ) ),
inference(resolve,[status(thm)],[c_77,c_39]) ).
cnf(c_247,plain,
aElement0(xb),
inference(resolve,[status(thm)],[c_207,c_20953]) ).
cnf(c_256,plain,
sdtasdt0(xx,smndt0(sdtpldt0(xa,xb))) = smndt0(xx),
inference(resolve,[status(thm)],[c_85,c_42]) ).
cnf(c_396,plain,
aElement0(smndt0(xx)),
inference(resolve,[status(thm)],[c_106,c_42]) ).
cnf(c_398,plain,
aElement0(smndt0(sdtpldt0(xa,xb))),
inference(resolve,[status(thm)],[c_108,c_106]) ).
cnf(c_409,plain,
sdtpldt0(sdtpldt0(xa,xb),smndt0(sdtpldt0(xa,xb))) = sz00,
inference(resolve,[status(thm)],[c_108,c_99]) ).
cnf(c_20954,plain,
( ~ aElementOf0(B,xI)
| aElementOf0(B,A)
| sdtasasdt0(xI,xI) != A ),
inference(resolve,[status(thm)],[c_123,c_206]) ).
cnf(c_20955,plain,
( ~ aElementOf0(A,xI)
| aElementOf0(A,sdtasasdt0(xI,xI)) ),
inference(xxres,[status(thm)],[c_20954]) ).
cnf(c_836,plain,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),sdtasasdt0(xI,xI)),
inference(resolve,[status(thm)],[c_20955,c_112]) ).
cnf(c_1014,plain,
aElement0(smndt0(xa)),
inference(resolve,[status(thm)],[c_246,c_106]) ).
cnf(c_1025,plain,
sdtpldt0(xa,smndt0(xa)) = sz00,
inference(resolve,[status(thm)],[c_246,c_99]) ).
cnf(c_1040,plain,
sdtasdt0(xa,smndt0(sdtpldt0(xa,xb))) = smndt0(xa),
inference(resolve,[status(thm)],[c_246,c_85]) ).
cnf(c_20956,plain,
( aElement0(sdtasdt0(xa,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_104,c_246]) ).
cnf(c_1130,plain,
aElement0(sdtasdt0(xa,xx)),
inference(resolve,[status(thm)],[c_20956,c_42]) ).
cnf(c_20957,plain,
( sdtasdt0(A,xx) = sdtasdt0(xx,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_97,c_42]) ).
cnf(c_20958,plain,
sdtasdt0(xa,xx) = sdtasdt0(xx,xa),
inference(resolve,[status(thm)],[c_20957,c_246]) ).
cnf(c_1162,plain,
sdtasdt0(xx,xa) = sdtasdt0(xa,xx),
inference(copy,[status(thm)],[c_20958]) ).
cnf(c_20959,plain,
( sdtasdt0(A,xy) = sdtasdt0(xy,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_97,c_41]) ).
cnf(c_20960,plain,
sdtasdt0(xa,xy) = sdtasdt0(xy,xa),
inference(resolve,[status(thm)],[c_20959,c_246]) ).
cnf(c_1163,plain,
sdtasdt0(xy,xa) = sdtasdt0(xa,xy),
inference(copy,[status(thm)],[c_20960]) ).
cnf(c_1259,plain,
aElementOf0(sdtasdt0(xa,xy),xI),
inference(paramod,[status(thm)],[c_1163,c_197]) ).
cnf(c_1260,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtasdt0(xa,xy),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),xI),
inference(paramod,[status(thm)],[c_1163,c_111]) ).
cnf(c_1313,plain,
sdtpldt0(xb,sz00) = xb,
inference(resolve,[status(thm)],[c_247,c_101]) ).
cnf(c_20961,plain,
( aElement0(sdtasdt0(xb,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_104,c_247]) ).
cnf(c_1447,plain,
aElement0(sdtasdt0(xb,xx)),
inference(resolve,[status(thm)],[c_20961,c_42]) ).
cnf(c_20962,plain,
( sdtpldt0(A,xa) = sdtpldt0(xa,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_103,c_246]) ).
cnf(c_1449,plain,
sdtpldt0(xb,xa) = sdtpldt0(xa,xb),
inference(resolve,[status(thm)],[c_20962,c_247]) ).
cnf(c_20963,plain,
( sdtasdt0(A,xx) = sdtasdt0(xx,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_97,c_42]) ).
cnf(c_20964,plain,
sdtasdt0(xb,xx) = sdtasdt0(xx,xb),
inference(resolve,[status(thm)],[c_20963,c_247]) ).
cnf(c_1497,plain,
sdtasdt0(xx,xb) = sdtasdt0(xb,xx),
inference(copy,[status(thm)],[c_20964]) ).
cnf(c_1717,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtasdt0(xa,xy),sdtpldt0(sdtasdt0(xb,xx),smndt0(xx))),xI),
inference(paramod,[status(thm)],[c_1497,c_1260]) ).
cnf(c_3123,plain,
sdtpldt0(smndt0(xa),sz00) = smndt0(xa),
inference(resolve,[status(thm)],[c_1014,c_101]) ).
cnf(c_20965,plain,
( sdtpldt0(A,sdtpldt0(xa,xb)) = sdtpldt0(sdtpldt0(xa,xb),A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_103,c_108]) ).
cnf(c_20966,plain,
sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)) = sdtpldt0(sdtpldt0(xa,xb),smndt0(xa)),
inference(resolve,[status(thm)],[c_20965,c_1014]) ).
cnf(c_3345,plain,
sdtpldt0(sdtpldt0(xa,xb),smndt0(xa)) = sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)),
inference(copy,[status(thm)],[c_20966]) ).
cnf(c_20967,plain,
( sdtpldt0(sdtpldt0(xb,A),B) = sdtpldt0(xb,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_102,c_247]) ).
cnf(c_20968,plain,
( sdtpldt0(sdtpldt0(xb,xa),A) = sdtpldt0(xb,sdtpldt0(xa,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20967,c_246]) ).
cnf(c_20969,plain,
sdtpldt0(sdtpldt0(xb,xa),smndt0(xa)) = sdtpldt0(xb,sdtpldt0(xa,smndt0(xa))),
inference(resolve,[status(thm)],[c_20968,c_1014]) ).
cnf(c_20970,plain,
sdtpldt0(sdtpldt0(xa,xb),smndt0(xa)) = sdtpldt0(xb,sdtpldt0(xa,smndt0(xa))),
inference(paramod,[status(thm)],[c_1449,c_20969]) ).
cnf(c_20971,plain,
sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)) = sdtpldt0(xb,sdtpldt0(xa,smndt0(xa))),
inference(paramod,[status(thm)],[c_3345,c_20970]) ).
cnf(c_20972,plain,
sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)) = sdtpldt0(xb,sz00),
inference(paramod,[status(thm)],[c_1025,c_20971]) ).
cnf(c_3368,plain,
sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)) = xb,
inference(paramod,[status(thm)],[c_1313,c_20972]) ).
cnf(c_14289,plain,
sdtasdt0(sdtasdt0(xa,xx),smndt0(sdtpldt0(xa,xb))) = smndt0(sdtasdt0(xa,xx)),
inference(resolve,[status(thm)],[c_1130,c_85]) ).
cnf(c_20973,plain,
( sdtpldt0(A,smndt0(xx)) = sdtpldt0(smndt0(xx),A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_103,c_396]) ).
cnf(c_16616,plain,
sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)) = sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)),
inference(resolve,[status(thm)],[c_20973,c_1447]) ).
cnf(c_16848,negated_conjecture,
~ aElementOf0(sdtpldt0(sdtasdt0(xa,xy),sdtpldt0(smndt0(xx),sdtasdt0(xb,xx))),xI),
inference(paramod,[status(thm)],[c_16616,c_1717]) ).
cnf(c_20974,plain,
( aElementOf0(sdtpldt0(A,B),xI)
| ~ aElementOf0(B,xI)
| ~ aElementOf0(A,xI) ),
inference(resolve,[status(thm)],[c_54,c_45]) ).
cnf(c_20975,plain,
( aElementOf0(sdtpldt0(sdtasdt0(xa,xy),A),xI)
| ~ aElementOf0(A,xI) ),
inference(resolve,[status(thm)],[c_20974,c_1259]) ).
cnf(c_17648,negated_conjecture,
~ aElementOf0(sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)),xI),
inference(resolve,[status(thm)],[c_20975,c_16848]) ).
cnf(c_20976,plain,
( aElementOf0(B,xI)
| ~ aElementOf0(B,A)
| sdtasasdt0(xI,xI) != A ),
inference(resolve,[status(thm)],[c_124,c_206]) ).
cnf(c_20977,plain,
( aElementOf0(A,xI)
| ~ aElementOf0(A,sdtasasdt0(xI,xI)) ),
inference(xxres,[status(thm)],[c_20976]) ).
cnf(c_17653,plain,
~ aElementOf0(sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)),sdtasasdt0(xI,xI)),
inference(resolve,[status(thm)],[c_20977,c_17648]) ).
cnf(c_20978,plain,
( sdtpldt0(sdtpldt0(smndt0(xa),A),B) = sdtpldt0(smndt0(xa),sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_102,c_1014]) ).
cnf(c_20979,plain,
( sdtpldt0(sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)),A) = sdtpldt0(smndt0(xa),sdtpldt0(sdtpldt0(xa,xb),A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20978,c_108]) ).
cnf(c_20980,plain,
sdtpldt0(sdtpldt0(smndt0(xa),sdtpldt0(xa,xb)),smndt0(sdtpldt0(xa,xb))) = sdtpldt0(smndt0(xa),sdtpldt0(sdtpldt0(xa,xb),smndt0(sdtpldt0(xa,xb)))),
inference(resolve,[status(thm)],[c_20979,c_398]) ).
cnf(c_20981,plain,
sdtpldt0(xb,smndt0(sdtpldt0(xa,xb))) = sdtpldt0(smndt0(xa),sdtpldt0(sdtpldt0(xa,xb),smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_3368,c_20980]) ).
cnf(c_20982,plain,
sdtpldt0(xb,smndt0(sdtpldt0(xa,xb))) = sdtpldt0(smndt0(xa),sz00),
inference(paramod,[status(thm)],[c_409,c_20981]) ).
cnf(c_19694,plain,
sdtpldt0(xb,smndt0(sdtpldt0(xa,xb))) = smndt0(xa),
inference(paramod,[status(thm)],[c_3123,c_20982]) ).
cnf(c_20983,plain,
( sdtasdt0(sdtasdt0(xx,A),B) = sdtasdt0(xx,sdtasdt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_96,c_42]) ).
cnf(c_20984,plain,
( sdtasdt0(sdtasdt0(xx,xa),A) = sdtasdt0(xx,sdtasdt0(xa,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20983,c_246]) ).
cnf(c_20985,plain,
sdtasdt0(sdtasdt0(xx,xa),smndt0(sdtpldt0(xa,xb))) = sdtasdt0(xx,sdtasdt0(xa,smndt0(sdtpldt0(xa,xb)))),
inference(resolve,[status(thm)],[c_20984,c_398]) ).
cnf(c_20986,plain,
sdtasdt0(sdtasdt0(xa,xx),smndt0(sdtpldt0(xa,xb))) = sdtasdt0(xx,sdtasdt0(xa,smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_1162,c_20985]) ).
cnf(c_20987,plain,
smndt0(sdtasdt0(xa,xx)) = sdtasdt0(xx,sdtasdt0(xa,smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_14289,c_20986]) ).
cnf(c_20988,plain,
smndt0(sdtasdt0(xa,xx)) = sdtasdt0(xx,smndt0(xa)),
inference(paramod,[status(thm)],[c_1040,c_20987]) ).
cnf(c_19740,plain,
sdtasdt0(xx,smndt0(xa)) = smndt0(sdtasdt0(xa,xx)),
inference(copy,[status(thm)],[c_20988]) ).
cnf(c_20989,plain,
( sdtpldt0(sdtasdt0(xx,A),sdtasdt0(xx,B)) = sdtasdt0(xx,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_91,c_42]) ).
cnf(c_20990,plain,
( sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(xx,A)) = sdtasdt0(xx,sdtpldt0(xb,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20989,c_247]) ).
cnf(c_20991,plain,
sdtpldt0(sdtasdt0(xx,xb),sdtasdt0(xx,smndt0(sdtpldt0(xa,xb)))) = sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),
inference(resolve,[status(thm)],[c_20990,c_398]) ).
cnf(c_20992,plain,
sdtpldt0(sdtasdt0(xb,xx),sdtasdt0(xx,smndt0(sdtpldt0(xa,xb)))) = sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_1497,c_20991]) ).
cnf(c_20993,plain,
sdtpldt0(sdtasdt0(xb,xx),smndt0(xx)) = sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_256,c_20992]) ).
cnf(c_20994,plain,
sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)) = sdtasdt0(xx,sdtpldt0(xb,smndt0(sdtpldt0(xa,xb)))),
inference(paramod,[status(thm)],[c_16616,c_20993]) ).
cnf(c_20995,plain,
sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)) = sdtasdt0(xx,smndt0(xa)),
inference(paramod,[status(thm)],[c_19694,c_20994]) ).
cnf(c_19966,plain,
sdtpldt0(smndt0(xx),sdtasdt0(xb,xx)) = smndt0(sdtasdt0(xa,xx)),
inference(paramod,[status(thm)],[c_19740,c_20995]) ).
cnf(c_20996,plain,
aElementOf0(sdtasdt0(xx,smndt0(xa)),sdtasasdt0(xI,xI)),
inference(paramod,[status(thm)],[c_19694,c_836]) ).
cnf(c_20226,plain,
aElementOf0(smndt0(sdtasdt0(xa,xx)),sdtasasdt0(xI,xI)),
inference(paramod,[status(thm)],[c_19740,c_20996]) ).
cnf(c_20997,plain,
~ aElementOf0(smndt0(sdtasdt0(xa,xx)),sdtasasdt0(xI,xI)),
inference(paramod,[status(thm)],[c_19966,c_17653]) ).
cnf(c_20946,plain,
$false,
inference(resolve,[status(thm)],[c_20226,c_20997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG098+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 06:00:05 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 16210 was started by sandbox on n017,
% 0.08/0.36 % Sat Sep 26 06:00:05 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 113.59/15.74
% 113.59/15.74 % SZS status Theorem for theBenchmark
% 113.59/15.74
% 113.59/15.74 % Proof 1 at 6.21 (+ 1.09) seconds.
% 113.59/15.74 % Length of proof is 91.
% 113.59/15.74 % Level of proof is 10.
% 113.59/15.74 % Maximum clause weight is 33.000.
% 113.59/15.74 % Given clauses 386.
% 113.59/15.74
% 113.59/15.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------