%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG071+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 : 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 : Sun Sep 27 08:26:33 AM UTC 2026
% Result : Theorem 49.39s 6.66s
% Output : CNFRefutation 49.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 24
% Syntax : Number of formulae : 128 ( 53 unt; 0 def)
% Number of atoms : 320 ( 43 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 332 ( 140 ~; 137 |; 41 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 16 con; 0-2 aty)
% Number of variables : 82 ( 2 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mScZero,axiom,
! [W0] :
( aScalar0(W0)
=> ( smndt0(sz0z00) = sz0z00
& smndt0(smndt0(W0)) = W0
& sdtpldt0(smndt0(W0),W0) = sz0z00
& sdtpldt0(W0,smndt0(W0)) = sz0z00
& sdtasdt0(sz0z00,W0) = sz0z00
& sdtasdt0(W0,sz0z00) = sz0z00
& sdtpldt0(sz0z00,W0) = W0
& sdtpldt0(W0,sz0z00) = W0 ) ),
file('theBenchmark.p',mScZero) ).
fof(mArith,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('theBenchmark.p',mArith) ).
fof(mLERef,axiom,
! [W0] :
( aScalar0(W0)
=> sdtlseqdt0(W0,W0) ),
file('theBenchmark.p',mLERef) ).
fof(mLETrn,axiom,
! [W0,W1,W2] :
( ( aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('theBenchmark.p',mLETrn) ).
fof(mLEMon,axiom,
! [W0,W1,W2,W3] :
( ( aScalar0(W3)
& aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(W2,W3)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ),
file('theBenchmark.p',mLEMon) ).
fof(mLEMonM,axiom,
! [W0,W1,W2,W3] :
( ( aScalar0(W3)
& aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(W2,W3)
& sdtlseqdt0(sz0z00,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ),
file('theBenchmark.p',mLEMonM) ).
fof(mLETot,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( sdtlseqdt0(W1,W0)
| sdtlseqdt0(W0,W1) ) ),
file('theBenchmark.p',mLETot) ).
fof(mPosMon,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(sz0z00,W1)
& sdtlseqdt0(sz0z00,W0) )
=> ( sdtlseqdt0(sz0z00,sdtasdt0(W0,W1))
& sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) ) ) ),
file('theBenchmark.p',mPosMon) ).
fof(mSqPos,axiom,
! [W0] :
( aScalar0(W0)
=> sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ),
file('theBenchmark.p',mSqPos) ).
fof(mScSqPos,axiom,
! [W0] :
( aVector0(W0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ),
file('theBenchmark.p',mScSqPos) ).
fof(m__1709,axiom,
( xp = sziznziztdt0(xs)
& aVector0(xp) ),
file('theBenchmark.p',m__1709) ).
fof(m__1726,axiom,
( xq = sziznziztdt0(xt)
& aVector0(xq) ),
file('theBenchmark.p',m__1726) ).
fof(m__1746,axiom,
( xA = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(xA) ),
file('theBenchmark.p',m__1746) ).
fof(m__1766,axiom,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ),
file('theBenchmark.p',m__1766) ).
fof(m__1783,axiom,
( xC = sdtasasdt0(xp,xp)
& aScalar0(xC) ),
file('theBenchmark.p',m__1783) ).
fof(m__1800,axiom,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
file('theBenchmark.p',m__1800) ).
fof(m__1837,axiom,
( xF = sdtasdt0(xA,xA)
& aScalar0(xF) ),
file('theBenchmark.p',m__1837) ).
fof(m__1854,axiom,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
file('theBenchmark.p',m__1854) ).
fof(m__1892,axiom,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
file('theBenchmark.p',m__1892) ).
fof(m__1911,axiom,
( xP = sdtasdt0(xE,xH)
& aScalar0(xP) ),
file('theBenchmark.p',m__1911) ).
fof(m__1930,axiom,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
file('theBenchmark.p',m__1930) ).
fof(m__,conjecture,
( sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
& sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
& sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mSZeroSc,axiom,
aScalar0(sz0z00),
file('theBenchmark.p',mSZeroSc) ).
cnf(c_60,plain,
aScalar0(sz0z00),
inference(clausify,[status(thm)],[mSZeroSc]) ).
cnf(c_64,plain,
( sdtpldt0(A,sz0z00) = A
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mScZero]) ).
cnf(c_66,plain,
( sdtasdt0(A,sz0z00) = sz0z00
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mScZero]) ).
cnf(c_73,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mArith]) ).
cnf(c_75,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mArith]) ).
cnf(c_85,plain,
( sdtlseqdt0(A,A)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLERef]) ).
cnf(c_87,plain,
( sdtlseqdt0(A,C)
| ~ sdtlseqdt0(B,C)
| ~ sdtlseqdt0(A,B)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLETrn]) ).
cnf(c_88,plain,
( sdtlseqdt0(sdtpldt0(A,C),sdtpldt0(B,D))
| ~ sdtlseqdt0(C,D)
| ~ sdtlseqdt0(A,B)
| ~ aScalar0(D)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLEMon]) ).
cnf(c_89,plain,
( sdtlseqdt0(sdtasdt0(A,C),sdtasdt0(B,D))
| ~ sdtlseqdt0(C,D)
| ~ sdtlseqdt0(sz0z00,C)
| ~ sdtlseqdt0(A,B)
| ~ aScalar0(D)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLEMonM]) ).
cnf(c_90,plain,
( sdtlseqdt0(B,A)
| sdtlseqdt0(A,B)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLETot]) ).
cnf(c_91,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(A,B))
| ~ sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mPosMon]) ).
cnf(c_93,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(A,A))
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mSqPos]) ).
cnf(c_107,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(A,A))
| ~ aVector0(A) ),
inference(clausify,[status(thm)],[mScSqPos]) ).
cnf(c_114,plain,
aVector0(xp),
inference(clausify,[status(thm)],[m__1709]) ).
cnf(c_116,plain,
aVector0(xq),
inference(clausify,[status(thm)],[m__1726]) ).
cnf(c_118,plain,
aScalar0(xA),
inference(clausify,[status(thm)],[m__1746]) ).
cnf(c_120,plain,
aScalar0(xB),
inference(clausify,[status(thm)],[m__1766]) ).
cnf(c_123,plain,
aScalar0(xC),
inference(clausify,[status(thm)],[m__1783]) ).
cnf(c_124,plain,
sdtasasdt0(xp,xp) = xC,
inference(clausify,[status(thm)],[m__1783]) ).
cnf(c_125,plain,
aScalar0(xD),
inference(clausify,[status(thm)],[m__1800]) ).
cnf(c_126,plain,
sdtasasdt0(xq,xq) = xD,
inference(clausify,[status(thm)],[m__1800]) ).
cnf(c_129,plain,
aScalar0(xF),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_130,plain,
sdtasdt0(xA,xA) = xF,
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_131,plain,
aScalar0(xG),
inference(clausify,[status(thm)],[m__1854]) ).
cnf(c_132,plain,
sdtasdt0(xB,xB) = xG,
inference(clausify,[status(thm)],[m__1854]) ).
cnf(c_135,plain,
aScalar0(xR),
inference(clausify,[status(thm)],[m__1892]) ).
cnf(c_136,plain,
sdtasdt0(xC,xG) = xR,
inference(clausify,[status(thm)],[m__1892]) ).
cnf(c_137,plain,
aScalar0(xP),
inference(clausify,[status(thm)],[m__1911]) ).
cnf(c_139,plain,
aScalar0(xS),
inference(clausify,[status(thm)],[m__1930]) ).
cnf(c_140,plain,
sdtasdt0(xF,xD) = xS,
inference(clausify,[status(thm)],[m__1930]) ).
fof(m__2590,axiom,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
file('theBenchmark.p',m__2590) ).
cnf(c_147,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(clausify,[status(thm)],[m__2590]) ).
cnf(c_149,negated_conjecture,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_155,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(factor,[status(thm)],[c_73]) ).
cnf(c_159,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(factor,[status(thm)],[c_75]) ).
cnf(c_176,plain,
( sdtlseqdt0(sdtpldt0(A,A),sdtpldt0(B,C))
| ~ sdtlseqdt0(A,C)
| ~ sdtlseqdt0(A,B)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(factor,[status(thm)],[c_88]) ).
cnf(c_183,plain,
( sdtlseqdt0(sdtasdt0(A,A),sdtasdt0(B,C))
| ~ sdtlseqdt0(A,C)
| ~ sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(A,B)
| ~ aScalar0(C)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(factor,[status(thm)],[c_89]) ).
cnf(c_28209,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(A,A))
| ~ sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(A) ),
inference(factor,[status(thm)],[c_91]) ).
cnf(c_191,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(A,A))
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(A) ),
inference(copy,[status(thm)],[c_28209]) ).
cnf(c_242,plain,
sdtpldt0(sz0z00,sz0z00) = sz0z00,
inference(resolve,[status(thm)],[c_64,c_60]) ).
cnf(c_243,plain,
sdtasdt0(sz0z00,sz0z00) = sz0z00,
inference(resolve,[status(thm)],[c_66,c_60]) ).
cnf(c_301,plain,
sdtlseqdt0(sz0z00,sz0z00),
inference(resolve,[status(thm)],[c_85,c_60]) ).
cnf(c_28210,plain,
sdtlseqdt0(sz0z00,sdtasasdt0(xp,xp)),
inference(resolve,[status(thm)],[c_114,c_107]) ).
cnf(c_355,plain,
sdtlseqdt0(sz0z00,xC),
inference(paramod,[status(thm)],[c_124,c_28210]) ).
cnf(c_28211,plain,
sdtlseqdt0(sz0z00,sdtasasdt0(xq,xq)),
inference(resolve,[status(thm)],[c_116,c_107]) ).
cnf(c_375,plain,
sdtlseqdt0(sz0z00,xD),
inference(paramod,[status(thm)],[c_126,c_28211]) ).
cnf(c_28212,plain,
sdtlseqdt0(sz0z00,sdtasdt0(xA,xA)),
inference(resolve,[status(thm)],[c_118,c_93]) ).
cnf(c_394,plain,
sdtlseqdt0(sz0z00,xF),
inference(paramod,[status(thm)],[c_130,c_28212]) ).
cnf(c_28213,plain,
sdtlseqdt0(sz0z00,sdtasdt0(xB,xB)),
inference(resolve,[status(thm)],[c_120,c_93]) ).
cnf(c_489,plain,
sdtlseqdt0(sz0z00,xG),
inference(paramod,[status(thm)],[c_132,c_28213]) ).
cnf(c_28214,plain,
( sdtlseqdt0(A,xR)
| sdtlseqdt0(xR,A)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_90,c_135]) ).
cnf(c_16737,plain,
( sdtlseqdt0(xP,xR)
| sdtlseqdt0(xR,xP) ),
inference(resolve,[status(thm)],[c_28214,c_137]) ).
cnf(c_28215,plain,
( sdtlseqdt0(A,xP)
| sdtlseqdt0(xP,A)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_90,c_137]) ).
cnf(c_18298,plain,
( sdtlseqdt0(xS,xP)
| sdtlseqdt0(xP,xS) ),
inference(resolve,[status(thm)],[c_28215,c_139]) ).
cnf(c_28216,plain,
( sdtpldt0(A,xS) = sdtpldt0(xS,A)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_155,c_139]) ).
cnf(c_28217,plain,
sdtpldt0(xR,xS) = sdtpldt0(xS,xR),
inference(resolve,[status(thm)],[c_28216,c_135]) ).
cnf(c_21430,plain,
sdtpldt0(xS,xR) = sdtpldt0(xR,xS),
inference(copy,[status(thm)],[c_28217]) ).
cnf(c_28218,plain,
( sdtasdt0(A,xF) = sdtasdt0(xF,A)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_159,c_129]) ).
cnf(c_28219,plain,
sdtasdt0(xD,xF) = sdtasdt0(xF,xD),
inference(resolve,[status(thm)],[c_28218,c_125]) ).
cnf(c_23360,plain,
sdtasdt0(xD,xF) = xS,
inference(paramod,[status(thm)],[c_140,c_28219]) ).
cnf(c_28220,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(A,B))
| ~ sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_183,c_60]) ).
cnf(c_28221,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xD,A))
| ~ sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28220,c_125]) ).
cnf(c_28222,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xD,xF))
| ~ sdtlseqdt0(sz0z00,xF)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,xD) ),
inference(resolve,[status(thm)],[c_28221,c_129]) ).
cnf(c_28223,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xD,xF))
| ~ sdtlseqdt0(sz0z00,xF)
| ~ sdtlseqdt0(sz0z00,sz0z00) ),
inference(resolve,[status(thm)],[c_28222,c_375]) ).
cnf(c_28224,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xD,xF))
| ~ sdtlseqdt0(sz0z00,xF) ),
inference(resolve,[status(thm)],[c_28223,c_301]) ).
cnf(c_28225,plain,
sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xD,xF)),
inference(resolve,[status(thm)],[c_28224,c_394]) ).
cnf(c_28226,plain,
sdtlseqdt0(sz0z00,sdtasdt0(xD,xF)),
inference(paramod,[status(thm)],[c_243,c_28225]) ).
cnf(c_27324,plain,
sdtlseqdt0(sz0z00,xS),
inference(paramod,[status(thm)],[c_23360,c_28226]) ).
cnf(c_28227,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(A,B))
| ~ sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_183,c_60]) ).
cnf(c_28228,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xC,A))
| ~ sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,xC)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28227,c_123]) ).
cnf(c_28229,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xC,xG))
| ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,xC) ),
inference(resolve,[status(thm)],[c_28228,c_131]) ).
cnf(c_28230,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xC,xG))
| ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(sz0z00,sz0z00) ),
inference(resolve,[status(thm)],[c_28229,c_355]) ).
cnf(c_28231,plain,
( sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xC,xG))
| ~ sdtlseqdt0(sz0z00,xG) ),
inference(resolve,[status(thm)],[c_28230,c_301]) ).
cnf(c_28232,plain,
sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xC,xG)),
inference(resolve,[status(thm)],[c_28231,c_489]) ).
cnf(c_28233,plain,
sdtlseqdt0(sz0z00,sdtasdt0(xC,xG)),
inference(paramod,[status(thm)],[c_243,c_28232]) ).
cnf(c_27394,plain,
sdtlseqdt0(sz0z00,xR),
inference(paramod,[status(thm)],[c_136,c_28233]) ).
cnf(c_28234,plain,
( sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(A,B))
| ~ sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_176,c_60]) ).
cnf(c_28235,plain,
( sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(xS,A))
| ~ sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28234,c_139]) ).
cnf(c_28236,plain,
( sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(xS,xR))
| ~ sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xS) ),
inference(resolve,[status(thm)],[c_28235,c_135]) ).
cnf(c_28237,plain,
( sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(xS,xR))
| ~ sdtlseqdt0(sz0z00,xR) ),
inference(resolve,[status(thm)],[c_28236,c_27324]) ).
cnf(c_28238,plain,
sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(xS,xR)),
inference(resolve,[status(thm)],[c_28237,c_27394]) ).
cnf(c_28239,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xS,xR)),
inference(paramod,[status(thm)],[c_242,c_28238]) ).
cnf(c_27876,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(paramod,[status(thm)],[c_21430,c_28239]) ).
cnf(c_27884,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)),
inference(resolve,[status(thm)],[c_27876,c_149]) ).
cnf(c_28240,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| ~ sdtlseqdt0(sz0z00,xP) ),
inference(resolve,[status(thm)],[c_191,c_137]) ).
cnf(c_28054,negated_conjecture,
~ sdtlseqdt0(sz0z00,xP),
inference(resolve,[status(thm)],[c_28240,c_27884]) ).
cnf(c_28241,plain,
( sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(A,B)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_87,c_60]) ).
cnf(c_28242,plain,
( sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(xS,A)
| ~ sdtlseqdt0(sz0z00,xS)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28241,c_139]) ).
cnf(c_28243,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xS,xP)
| ~ sdtlseqdt0(sz0z00,xS) ),
inference(resolve,[status(thm)],[c_28242,c_137]) ).
cnf(c_28244,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xS,xP) ),
inference(resolve,[status(thm)],[c_28243,c_27324]) ).
cnf(c_28057,plain,
~ sdtlseqdt0(xS,xP),
inference(resolve,[status(thm)],[c_28244,c_28054]) ).
cnf(c_28245,plain,
( sdtlseqdt0(sz0z00,B)
| ~ sdtlseqdt0(A,B)
| ~ sdtlseqdt0(sz0z00,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_87,c_60]) ).
cnf(c_28246,plain,
( sdtlseqdt0(sz0z00,A)
| ~ sdtlseqdt0(xR,A)
| ~ sdtlseqdt0(sz0z00,xR)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28245,c_135]) ).
cnf(c_28247,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xR,xP)
| ~ sdtlseqdt0(sz0z00,xR) ),
inference(resolve,[status(thm)],[c_28246,c_137]) ).
cnf(c_28248,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(xR,xP) ),
inference(resolve,[status(thm)],[c_28247,c_27394]) ).
cnf(c_28058,plain,
~ sdtlseqdt0(xR,xP),
inference(resolve,[status(thm)],[c_28248,c_28054]) ).
cnf(c_28064,plain,
sdtlseqdt0(xP,xS),
inference(resolve,[status(thm)],[c_28057,c_18298]) ).
cnf(c_28065,plain,
sdtlseqdt0(xP,xR),
inference(resolve,[status(thm)],[c_28058,c_16737]) ).
cnf(c_28249,plain,
( sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(A,B))
| ~ sdtlseqdt0(xP,B)
| ~ sdtlseqdt0(xP,A)
| ~ aScalar0(B)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_176,c_137]) ).
cnf(c_28250,plain,
( sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,A))
| ~ sdtlseqdt0(xP,A)
| ~ sdtlseqdt0(xP,xR)
| ~ aScalar0(A) ),
inference(resolve,[status(thm)],[c_28249,c_135]) ).
cnf(c_28251,plain,
( sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))
| ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,xR) ),
inference(resolve,[status(thm)],[c_28250,c_139]) ).
cnf(c_28252,plain,
( sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))
| ~ sdtlseqdt0(xP,xR) ),
inference(resolve,[status(thm)],[c_28251,c_28064]) ).
cnf(c_28253,plain,
~ sdtlseqdt0(xP,xR),
inference(resolve,[status(thm)],[c_28252,c_147]) ).
cnf(c_28208,plain,
$false,
inference(resolve,[status(thm)],[c_28065,c_28253]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG071+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.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 05:58:14 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3513215 was started by sandbox on n009,
% 0.09/0.37 % Sat Sep 26 05:58:14 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 49.39/6.66
% 49.39/6.66 % SZS status Theorem for theBenchmark
% 49.39/6.66
% 49.39/6.66 % Proof 1 at 5.29 (+ 0.89) seconds.
% 49.39/6.66 % Length of proof is 80.
% 49.39/6.66 % Level of proof is 10.
% 49.39/6.66 % Maximum clause weight is 34.000.
% 49.39/6.66 % Given clauses 201.
% 49.39/6.66
% 49.39/6.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------