%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG119+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Sun Sep 27 08:26:42 AM UTC 2026
% Result : Theorem 182.34s 29.63s
% Output : CNFRefutation 182.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 16
% Syntax : Number of formulae : 145 ( 83 unt; 0 def)
% Number of atoms : 343 ( 163 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 299 ( 101 ~; 93 |; 86 &)
% ( 5 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 113 ( 0 sgn 34 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
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(mMulComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
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(mMulZero,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('theBenchmark.p',mMulZero) ).
fof(mCancel,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('theBenchmark.p',mCancel) ).
fof(mEOfElem,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('theBenchmark.p',mEOfElem) ).
fof(mDefPrIdeal,axiom,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) ) ),
file('theBenchmark.p',mDefPrIdeal) ).
fof(m__2091,axiom,
( aElement0(xb)
& aElement0(xa) ),
file('theBenchmark.p',m__2091) ).
fof(m__2174,axiom,
( xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))
& ! [W0] :
( aElementOf0(W0,xI)
<=> ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xb))
<=> ? [W1] :
( sdtasdt0(xb,W1) = W0
& aElement0(W1) ) )
& ! [W0] :
( aElementOf0(W0,slsdtgt0(xa))
<=> ? [W1] :
( sdtasdt0(xa,W1) = W0
& aElement0(W1) ) )
& aIdeal0(xI)
& ! [W0] :
( aElementOf0(W0,xI)
=> ( ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xI) )
& ! [W1] :
( aElementOf0(W1,xI)
=> aElementOf0(sdtpldt0(W0,W1),xI) ) ) )
& aSet0(xI) ),
file('theBenchmark.p',m__2174) ).
fof(m__2203,axiom,
( aElementOf0(xb,slsdtgt0(xb))
& ? [W0] :
( sdtasdt0(xb,W0) = xb
& aElement0(W0) )
& aElementOf0(sz00,slsdtgt0(xb))
& ? [W0] :
( sdtasdt0(xb,W0) = sz00
& aElement0(W0) )
& aElementOf0(xa,slsdtgt0(xa))
& ? [W0] :
( sdtasdt0(xa,W0) = xa
& aElement0(W0) )
& aElementOf0(sz00,slsdtgt0(xa))
& ? [W0] :
( sdtasdt0(xa,W0) = sz00
& aElement0(W0) ) ),
file('theBenchmark.p',m__2203) ).
fof(m__2273,axiom,
( ! [W0] :
( ( W0 != sz00
& ( aElementOf0(W0,xI)
| ? [W1,W2] :
( sdtpldt0(W1,W2) = W0
& aElementOf0(W2,slsdtgt0(xb))
& aElementOf0(W1,slsdtgt0(xa)) ) ) )
=> ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [W0,W1] :
( sdtpldt0(W0,W1) = xu
& aElementOf0(W1,slsdtgt0(xb))
& aElementOf0(W0,slsdtgt0(xa)) ) ),
file('theBenchmark.p',m__2273) ).
fof(m__2612,axiom,
~ ( doDivides0(xu,xb)
| ? [W0] :
( sdtasdt0(xu,W0) = xb
& aElement0(W0) ) ),
file('theBenchmark.p',m__2612) ).
fof(m__2666,axiom,
( ( iLess0(sbrdtbr0(xr),sbrdtbr0(xu))
| xr = sz00 )
& xb = sdtpldt0(sdtasdt0(xq,xu),xr)
& aElement0(xr)
& aElement0(xq) ),
file('theBenchmark.p',m__2666) ).
fof(m__,conjecture,
xr != sz00,
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( xr != sz00 ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mSortsC,axiom,
aElement0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_72,plain,
aElement0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_78,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_79,plain,
( sdtpldt0(A,sz00) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_80,plain,
( sdtpldt0(sz00,A) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_83,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_87,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_88,plain,
( sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C)) = sdtasdt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_87]) ).
cnf(c_89,plain,
( sdtasdt0(sdtpldt0(B,C),A) = sdtpldt0(sdtasdt0(B,A),sdtasdt0(C,A))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAMDistr]) ).
cnf(c_90,plain,
( sdtpldt0(sdtasdt0(B,A),sdtasdt0(C,A)) = sdtasdt0(sdtpldt0(B,C),A)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_89]) ).
cnf(c_93,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulZero]) ).
cnf(c_94,plain,
( sdtasdt0(sz00,A) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulZero]) ).
cnf(c_95,plain,
( B = sz00
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mCancel]) ).
cnf(c_96,plain,
( sz00 = B
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_95]) ).
cnf(c_98,plain,
( aElement0(B)
| ~ aElementOf0(B,A)
| ~ aSet0(A) ),
inference(clausify,[status(thm)],[mEOfElem]) ).
cnf(c_146,plain,
( aSet0(B)
| slsdtgt0(A) != B
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mDefPrIdeal]) ).
cnf(c_155,plain,
aElement0(xa),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_156,plain,
aElement0(xb),
inference(clausify,[status(thm)],[m__2091]) ).
cnf(c_194,plain,
aSet0(xI),
inference(clausify,[status(thm)],[m__2174]) ).
fof(nnf_39,plain,
( aElementOf0(xb,slsdtgt0(xb))
& ? [W0] :
( sdtasdt0(xb,W0) = xb
& aElement0(W0) )
& aElementOf0(sz00,slsdtgt0(xb))
& ? [X3] :
( sdtasdt0(xb,X3) = sz00
& aElement0(X3) )
& aElementOf0(xa,slsdtgt0(xa))
& ? [X0] :
( sdtasdt0(xa,X0) = xa
& aElement0(X0) )
& aElementOf0(sz00,slsdtgt0(xa))
& ? [X2] :
( sdtasdt0(xa,X2) = sz00
& aElement0(X2) ) ),
inference(fof_nnf,[status(thm)],[m__2203]) ).
fof(sk_m__2203,plain,
( aElementOf0(xb,slsdtgt0(xb))
& sdtasdt0(xb,sK12) = xb
& aElement0(sK12)
& aElementOf0(sz00,slsdtgt0(xb))
& sdtasdt0(xb,sK0) = sz00
& aElement0(sK0)
& aElementOf0(xa,slsdtgt0(xa))
& sdtasdt0(xa,sK11) = xa
& aElement0(sK11)
& aElementOf0(sz00,slsdtgt0(xa))
& sdtasdt0(xa,sK10) = sz00
& aElement0(sK10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK0,sK12]),skolemize(X2,sK10),skolemize(X0,sK11),skolemize(X3,sK0),skolemize(W0,sK12)],[nnf_39]) ).
cnf(c_215,plain,
aElement0(sK0),
inference(split_conjunct,[status(thm)],[sk_m__2203]) ).
cnf(c_216,plain,
sdtasdt0(xb,sK0) = sz00,
inference(split_conjunct,[status(thm)],[sk_m__2203]) ).
fof(nnf_41,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| sz00 = W0
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& ? [X3,X0] :
( sdtpldt0(X3,X0) = xu
& aElementOf0(X0,slsdtgt0(xb))
& aElementOf0(X3,slsdtgt0(xa)) ) ),
inference(fof_nnf,[status(thm)],[m__2273]) ).
fof(sk_m__2273_sk,plain,
( ! [W0] :
( ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu))
| sz00 = W0
| ( ~ aElementOf0(W0,xI)
& ! [W1,W2] :
( sdtpldt0(W1,W2) != W0
| ~ aElementOf0(W2,slsdtgt0(xb))
| ~ aElementOf0(W1,slsdtgt0(xa)) ) ) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sK1,sK2) = xu
& aElementOf0(sK2,slsdtgt0(xb))
& aElementOf0(sK1,slsdtgt0(xa)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X3,sK1),skolemize(X0,sK2)],[nnf_41]) ).
fof(sk_m__2273,plain,
( ! [VAR_0] :
( ~ iLess0(sbrdtbr0(VAR_0),sbrdtbr0(xu))
| sz00 = VAR_0
| ~ aElementOf0(VAR_0,xI) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ iLess0(sbrdtbr0(VAR_2),sbrdtbr0(xu))
| sz00 = VAR_2
| sdtpldt0(VAR_0,VAR_1) != VAR_2
| ~ aElementOf0(VAR_1,slsdtgt0(xb))
| ~ aElementOf0(VAR_0,slsdtgt0(xa)) )
& xu != sz00
& aElementOf0(xu,xI)
& sdtpldt0(sK1,sK2) = xu
& aElementOf0(sK2,slsdtgt0(xb))
& aElementOf0(sK1,slsdtgt0(xa)) ),
inference(cnf_transformation,[status(thm)],[sk_m__2273_sk]) ).
cnf(c_233,plain,
aElementOf0(sK1,slsdtgt0(xa)),
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_234,plain,
aElementOf0(sK2,slsdtgt0(xb)),
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_235,plain,
sdtpldt0(sK1,sK2) = xu,
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_236,plain,
aElementOf0(xu,xI),
inference(split_conjunct,[status(thm)],[sk_m__2273]) ).
cnf(c_255,plain,
( sdtasdt0(xu,A) != xb
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m__2612]) ).
cnf(c_257,plain,
aElement0(xq),
inference(clausify,[status(thm)],[m__2666]) ).
cnf(c_259,plain,
sdtpldt0(sdtasdt0(xq,xu),xr) = xb,
inference(clausify,[status(thm)],[m__2666]) ).
cnf(c_261,negated_conjecture,
xr = sz00,
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_362,plain,
sdtpldt0(sdtasdt0(xq,xu),sz00) = xb,
inference(paramod,[status(thm)],[c_261,c_259]) ).
cnf(c_470,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(resolve,[status(thm)],[c_79,c_72]) ).
cnf(c_25067,plain,
( aSet0(A)
| slsdtgt0(xa) != A ),
inference(resolve,[status(thm)],[c_146,c_155]) ).
cnf(c_741,plain,
aSet0(slsdtgt0(xa)),
inference(xxres,[status(thm)],[c_25067]) ).
cnf(c_882,plain,
sdtasdt0(sz00,xb) = sz00,
inference(resolve,[status(thm)],[c_156,c_94]) ).
cnf(c_25068,plain,
( aSet0(A)
| slsdtgt0(xb) != A ),
inference(resolve,[status(thm)],[c_146,c_156]) ).
cnf(c_921,plain,
aSet0(slsdtgt0(xb)),
inference(xxres,[status(thm)],[c_25068]) ).
cnf(c_6362,plain,
sdtpldt0(sz00,sK0) = sK0,
inference(resolve,[status(thm)],[c_215,c_80]) ).
cnf(c_25069,plain,
( sdtasdt0(A,xb) = sdtasdt0(xb,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_156]) ).
cnf(c_25070,plain,
sdtasdt0(sK0,xb) = sdtasdt0(xb,sK0),
inference(resolve,[status(thm)],[c_25069,c_215]) ).
cnf(c_7209,plain,
sdtasdt0(sK0,xb) = sz00,
inference(paramod,[status(thm)],[c_216,c_25070]) ).
cnf(c_25071,plain,
( sz00 = sK0
| sz00 = xb
| ~ aElement0(sK0)
| ~ aElement0(xb) ),
inference(resolve,[status(thm)],[c_216,c_96]) ).
cnf(c_25072,plain,
( sz00 = sK0
| xb = sz00
| ~ aElement0(sK0)
| ~ aElement0(xb) ),
inference(copy,[status(thm)],[c_25071]) ).
cnf(c_25073,plain,
( sz00 = sK0
| xb = sz00
| ~ aElement0(sK0) ),
inference(resolve,[status(thm)],[c_156,c_25072]) ).
cnf(c_8021,plain,
( sz00 = sK0
| xb = sz00 ),
inference(resolve,[status(thm)],[c_215,c_25073]) ).
cnf(c_25074,plain,
( aElement0(sK1)
| ~ aSet0(slsdtgt0(xa)) ),
inference(resolve,[status(thm)],[c_233,c_98]) ).
cnf(c_10373,plain,
aElement0(sK1),
inference(resolve,[status(thm)],[c_741,c_25074]) ).
cnf(c_25075,plain,
( aElement0(sK2)
| ~ aSet0(slsdtgt0(xb)) ),
inference(resolve,[status(thm)],[c_234,c_98]) ).
cnf(c_10408,plain,
aElement0(sK2),
inference(resolve,[status(thm)],[c_921,c_25075]) ).
cnf(c_25076,plain,
( aElement0(xu)
| ~ aSet0(xI) ),
inference(resolve,[status(thm)],[c_236,c_98]) ).
cnf(c_10443,plain,
aElement0(xu),
inference(resolve,[status(thm)],[c_194,c_25076]) ).
cnf(c_16995,plain,
sdtasdt0(xu,sz00) != xb,
inference(resolve,[status(thm)],[c_255,c_72]) ).
cnf(c_16996,plain,
sdtasdt0(xu,xq) != xb,
inference(resolve,[status(thm)],[c_257,c_255]) ).
cnf(c_17058,plain,
sdtasdt0(sz00,xq) = sz00,
inference(resolve,[status(thm)],[c_257,c_94]) ).
cnf(c_25077,plain,
( sdtpldt0(sdtasdt0(A,xq),sdtasdt0(B,xq)) = sdtasdt0(sdtpldt0(A,B),xq)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_90,c_257]) ).
cnf(c_25078,plain,
( sdtpldt0(sdtasdt0(sz00,xq),sdtasdt0(A,xq)) = sdtasdt0(sdtpldt0(sz00,A),xq)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25077,c_72]) ).
cnf(c_25079,plain,
sdtpldt0(sdtasdt0(sz00,xq),sdtasdt0(sK0,xq)) = sdtasdt0(sdtpldt0(sz00,sK0),xq),
inference(resolve,[status(thm)],[c_25078,c_215]) ).
cnf(c_25080,plain,
sdtpldt0(sz00,sdtasdt0(sK0,xq)) = sdtasdt0(sdtpldt0(sz00,sK0),xq),
inference(paramod,[status(thm)],[c_17058,c_25079]) ).
cnf(c_17827,plain,
sdtpldt0(sz00,sdtasdt0(sK0,xq)) = sdtasdt0(sK0,xq),
inference(paramod,[status(thm)],[c_6362,c_25080]) ).
cnf(c_25081,plain,
( sdtpldt0(sdtasdt0(sK0,A),sdtasdt0(sK0,B)) = sdtasdt0(sK0,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_88,c_215]) ).
cnf(c_25082,plain,
( sdtpldt0(sdtasdt0(sK0,xb),sdtasdt0(sK0,A)) = sdtasdt0(sK0,sdtpldt0(xb,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25081,c_156]) ).
cnf(c_25083,plain,
sdtpldt0(sdtasdt0(sK0,xb),sdtasdt0(sK0,xq)) = sdtasdt0(sK0,sdtpldt0(xb,xq)),
inference(resolve,[status(thm)],[c_25082,c_257]) ).
cnf(c_25084,plain,
sdtpldt0(sz00,sdtasdt0(sK0,xq)) = sdtasdt0(sK0,sdtpldt0(xb,xq)),
inference(paramod,[status(thm)],[c_7209,c_25083]) ).
cnf(c_25085,plain,
sdtasdt0(sK0,xq) = sdtasdt0(sK0,sdtpldt0(xb,xq)),
inference(paramod,[status(thm)],[c_17827,c_25084]) ).
cnf(c_17910,plain,
sdtasdt0(sK0,sdtpldt0(xb,xq)) = sdtasdt0(sK0,xq),
inference(copy,[status(thm)],[c_25085]) ).
cnf(c_25086,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_88,c_72]) ).
cnf(c_25087,plain,
( sdtpldt0(sdtasdt0(sz00,xb),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(xb,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25086,c_156]) ).
cnf(c_25088,plain,
sdtpldt0(sdtasdt0(sz00,xb),sdtasdt0(sz00,xq)) = sdtasdt0(sz00,sdtpldt0(xb,xq)),
inference(resolve,[status(thm)],[c_25087,c_257]) ).
cnf(c_25089,plain,
sdtpldt0(sz00,sdtasdt0(sz00,xq)) = sdtasdt0(sz00,sdtpldt0(xb,xq)),
inference(paramod,[status(thm)],[c_882,c_25088]) ).
cnf(c_25090,plain,
sdtpldt0(sz00,sz00) = sdtasdt0(sz00,sdtpldt0(xb,xq)),
inference(paramod,[status(thm)],[c_17058,c_25089]) ).
cnf(c_25091,plain,
sz00 = sdtasdt0(sz00,sdtpldt0(xb,xq)),
inference(paramod,[status(thm)],[c_470,c_25090]) ).
cnf(c_18027,plain,
sdtasdt0(sz00,sdtpldt0(xb,xq)) = sz00,
inference(copy,[status(thm)],[c_25091]) ).
cnf(c_21436,plain,
sdtasdt0(sK1,sz00) = sz00,
inference(resolve,[status(thm)],[c_10373,c_93]) ).
cnf(c_25092,plain,
( sdtasdt0(A,xq) = sdtasdt0(xq,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_257]) ).
cnf(c_25093,plain,
sdtasdt0(sK1,xq) = sdtasdt0(xq,sK1),
inference(resolve,[status(thm)],[c_25092,c_10373]) ).
cnf(c_22032,plain,
sdtasdt0(xq,sK1) = sdtasdt0(sK1,xq),
inference(copy,[status(thm)],[c_25093]) ).
cnf(c_22310,plain,
sdtasdt0(sK2,sz00) = sz00,
inference(resolve,[status(thm)],[c_10408,c_93]) ).
cnf(c_22319,plain,
sdtpldt0(sK2,sz00) = sK2,
inference(resolve,[status(thm)],[c_10408,c_79]) ).
cnf(c_25094,plain,
( sdtpldt0(sdtasdt0(A,xq),sdtasdt0(B,xq)) = sdtasdt0(sdtpldt0(A,B),xq)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_90,c_257]) ).
cnf(c_25095,plain,
( sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(A,xq)) = sdtasdt0(sdtpldt0(sK1,A),xq)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25094,c_10373]) ).
cnf(c_25096,plain,
sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(sK2,xq)) = sdtasdt0(sdtpldt0(sK1,sK2),xq),
inference(resolve,[status(thm)],[c_25095,c_10408]) ).
cnf(c_22501,plain,
sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(sK2,xq)) = sdtasdt0(xu,xq),
inference(paramod,[status(thm)],[c_235,c_25096]) ).
cnf(c_25097,plain,
( sdtpldt0(sdtasdt0(A,sz00),sdtasdt0(B,sz00)) = sdtasdt0(sdtpldt0(A,B),sz00)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_90,c_72]) ).
cnf(c_25098,plain,
( sdtpldt0(sdtasdt0(sK1,sz00),sdtasdt0(A,sz00)) = sdtasdt0(sdtpldt0(sK1,A),sz00)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25097,c_10373]) ).
cnf(c_25099,plain,
sdtpldt0(sdtasdt0(sK1,sz00),sdtasdt0(sK2,sz00)) = sdtasdt0(sdtpldt0(sK1,sK2),sz00),
inference(resolve,[status(thm)],[c_25098,c_10408]) ).
cnf(c_25100,plain,
sdtpldt0(sz00,sdtasdt0(sK2,sz00)) = sdtasdt0(sdtpldt0(sK1,sK2),sz00),
inference(paramod,[status(thm)],[c_21436,c_25099]) ).
cnf(c_25101,plain,
sdtpldt0(sz00,sz00) = sdtasdt0(sdtpldt0(sK1,sK2),sz00),
inference(paramod,[status(thm)],[c_22310,c_25100]) ).
cnf(c_25102,plain,
sz00 = sdtasdt0(sdtpldt0(sK1,sK2),sz00),
inference(paramod,[status(thm)],[c_470,c_25101]) ).
cnf(c_25103,plain,
sz00 = sdtasdt0(xu,sz00),
inference(paramod,[status(thm)],[c_235,c_25102]) ).
cnf(c_22568,plain,
sdtasdt0(xu,sz00) = sz00,
inference(copy,[status(thm)],[c_25103]) ).
cnf(c_25104,plain,
( sdtpldt0(sdtasdt0(xq,A),sdtasdt0(xq,B)) = sdtasdt0(xq,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_88,c_257]) ).
cnf(c_25105,plain,
( sdtpldt0(sdtasdt0(xq,sK1),sdtasdt0(xq,A)) = sdtasdt0(xq,sdtpldt0(sK1,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25104,c_10373]) ).
cnf(c_25106,plain,
sdtpldt0(sdtasdt0(xq,sK1),sdtasdt0(xq,sK2)) = sdtasdt0(xq,sdtpldt0(sK1,sK2)),
inference(resolve,[status(thm)],[c_25105,c_10408]) ).
cnf(c_25107,plain,
sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(xq,sK2)) = sdtasdt0(xq,sdtpldt0(sK1,sK2)),
inference(paramod,[status(thm)],[c_22032,c_25106]) ).
cnf(c_22731,plain,
sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(xq,sK2)) = sdtasdt0(xq,xu),
inference(paramod,[status(thm)],[c_235,c_25107]) ).
cnf(c_25108,plain,
( sdtasdt0(A,xq) = sdtasdt0(xq,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_83,c_257]) ).
cnf(c_25109,plain,
sdtasdt0(sK2,xq) = sdtasdt0(xq,sK2),
inference(resolve,[status(thm)],[c_25108,c_10408]) ).
cnf(c_22898,plain,
sdtasdt0(xq,sK2) = sdtasdt0(sK2,xq),
inference(copy,[status(thm)],[c_25109]) ).
cnf(c_25110,plain,
( sdtpldt0(sdtpldt0(sK1,A),B) = sdtpldt0(sK1,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_78,c_10373]) ).
cnf(c_25111,plain,
( sdtpldt0(sdtpldt0(sK1,sK2),A) = sdtpldt0(sK1,sdtpldt0(sK2,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25110,c_10408]) ).
cnf(c_25112,plain,
sdtpldt0(sdtpldt0(sK1,sK2),sz00) = sdtpldt0(sK1,sdtpldt0(sK2,sz00)),
inference(resolve,[status(thm)],[c_25111,c_72]) ).
cnf(c_25113,plain,
sdtpldt0(xu,sz00) = sdtpldt0(sK1,sdtpldt0(sK2,sz00)),
inference(paramod,[status(thm)],[c_235,c_25112]) ).
cnf(c_25114,plain,
sdtpldt0(xu,sz00) = sdtpldt0(sK1,sK2),
inference(paramod,[status(thm)],[c_22319,c_25113]) ).
cnf(c_22912,plain,
sdtpldt0(xu,sz00) = xu,
inference(paramod,[status(thm)],[c_235,c_25114]) ).
cnf(c_25115,plain,
sz00 != xb,
inference(paramod,[status(thm)],[c_22568,c_16995]) ).
cnf(c_22967,plain,
xb != sz00,
inference(copy,[status(thm)],[c_25115]) ).
cnf(c_25116,plain,
sdtpldt0(sdtasdt0(sK1,xq),sdtasdt0(sK2,xq)) = sdtasdt0(xq,xu),
inference(paramod,[status(thm)],[c_22898,c_22731]) ).
cnf(c_22979,plain,
sdtasdt0(xu,xq) = sdtasdt0(xq,xu),
inference(paramod,[status(thm)],[c_22501,c_25116]) ).
cnf(c_23033,plain,
sz00 = sK0,
inference(resolve,[status(thm)],[c_22967,c_8021]) ).
cnf(c_23060,plain,
sdtasdt0(xq,xu) != xb,
inference(paramod,[status(thm)],[c_22979,c_16996]) ).
cnf(c_23080,plain,
sdtpldt0(xu,sK0) = xu,
inference(paramod,[status(thm)],[c_23033,c_22912]) ).
cnf(c_25117,plain,
sdtasdt0(sK0,sdtpldt0(xb,xq)) = sz00,
inference(paramod,[status(thm)],[c_23033,c_18027]) ).
cnf(c_25118,plain,
sdtasdt0(sK0,xq) = sz00,
inference(paramod,[status(thm)],[c_17910,c_25117]) ).
cnf(c_23613,plain,
sdtasdt0(sK0,xq) = sK0,
inference(paramod,[status(thm)],[c_23033,c_25118]) ).
cnf(c_24529,plain,
sdtpldt0(sdtasdt0(xq,xu),sK0) = xb,
inference(paramod,[status(thm)],[c_23033,c_362]) ).
cnf(c_25119,plain,
( sdtpldt0(sdtasdt0(A,xq),sdtasdt0(B,xq)) = sdtasdt0(sdtpldt0(A,B),xq)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_90,c_257]) ).
cnf(c_25120,plain,
( sdtpldt0(sdtasdt0(xu,xq),sdtasdt0(A,xq)) = sdtasdt0(sdtpldt0(xu,A),xq)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25119,c_10443]) ).
cnf(c_25121,plain,
sdtpldt0(sdtasdt0(xu,xq),sdtasdt0(sK0,xq)) = sdtasdt0(sdtpldt0(xu,sK0),xq),
inference(resolve,[status(thm)],[c_25120,c_215]) ).
cnf(c_25122,plain,
sdtpldt0(sdtasdt0(xq,xu),sdtasdt0(sK0,xq)) = sdtasdt0(sdtpldt0(xu,sK0),xq),
inference(paramod,[status(thm)],[c_22979,c_25121]) ).
cnf(c_25123,plain,
sdtpldt0(sdtasdt0(xq,xu),sK0) = sdtasdt0(sdtpldt0(xu,sK0),xq),
inference(paramod,[status(thm)],[c_23613,c_25122]) ).
cnf(c_25124,plain,
xb = sdtasdt0(sdtpldt0(xu,sK0),xq),
inference(paramod,[status(thm)],[c_24529,c_25123]) ).
cnf(c_25125,plain,
xb = sdtasdt0(xu,xq),
inference(paramod,[status(thm)],[c_23080,c_25124]) ).
cnf(c_25126,plain,
xb = sdtasdt0(xq,xu),
inference(paramod,[status(thm)],[c_22979,c_25125]) ).
cnf(c_25127,plain,
sdtasdt0(xq,xu) = xb,
inference(copy,[status(thm)],[c_25126]) ).
cnf(c_25066,plain,
$false,
inference(resolve,[status(thm)],[c_23060,c_25127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG119+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/5.48 % Computer : n008.cluster.edu
% 0.21/5.48 % Model : x86_64 x86_64
% 0.21/5.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/5.48 % Memory : 8046.5625MB
% 0.21/5.48 % OS : Linux 6.8.0-71-generic
% 0.21/5.48 % CPULimit : 300
% 0.21/5.48 % WCLimit : 300
% 0.21/5.48 % DateTime : Sat Sep 26 06:11:01 UTC 2026
% 0.21/5.48 % CPUTime :
% 0.21/5.48 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.21/5.48 % Process 2947991 was started by sandbox2 on n008,
% 0.21/5.48 % Sat Sep 26 06:11:01 2026
% 0.21/5.48 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.24/5.51
% 0.24/5.51 % From the command line: assign(max_seconds, 300).
% 182.34/29.63
% 182.34/29.63 % SZS status Theorem for theBenchmark
% 182.34/29.63
% 182.34/29.63 % Proof 1 at 6.37 (+ 1.57) seconds.
% 182.34/29.63 % Length of proof is 77.
% 182.34/29.63 % Level of proof is 9.
% 182.34/29.63 % Maximum clause weight is 42.000.
% 182.34/29.63 % Given clauses 305.
% 182.34/29.63
% 182.34/29.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------