%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : RNG071+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:25:46 AM UTC 2026
% Result : Theorem 5.73s 3.07s
% Output : CNFRefutation 5.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 21
% Syntax : Number of formulae : 102 ( 33 unt; 0 def)
% Number of atoms : 265 ( 37 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 287 ( 124 ~; 120 |; 30 &)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 16 con; 0-2 aty)
% Number of variables : 42 ( 0 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSZeroSc,axiom,
aScalar0(sz0z00) ).
fof(mLEASm,axiom,
! [X0,X1] :
( ( aScalar0(X1)
& aScalar0(X0) )
=> ( ( sdtlseqdt0(X1,X0)
& sdtlseqdt0(X0,X1) )
=> X0 = X1 ) ) ).
fof(mLETrn,axiom,
! [X0,X1,X2] :
( ( aScalar0(X2)
& aScalar0(X1)
& aScalar0(X0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X0,X1) )
=> sdtlseqdt0(X0,X2) ) ) ).
fof(mLEMon,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X3)
& aScalar0(X2)
& aScalar0(X1)
& aScalar0(X0) )
=> ( ( sdtlseqdt0(X2,X3)
& sdtlseqdt0(X0,X1) )
=> sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ) ) ).
fof(mLETot,axiom,
! [X0,X1] :
( ( aScalar0(X1)
& aScalar0(X0) )
=> ( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1) ) ) ).
fof(mPosMon,axiom,
! [X0,X1] :
( ( aScalar0(X1)
& aScalar0(X0) )
=> ( ( sdtlseqdt0(sz0z00,X1)
& sdtlseqdt0(sz0z00,X0) )
=> ( sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtpldt0(X0,X1)) ) ) ) ).
fof(mSqPos,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ) ).
fof(mScSqPos,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ) ).
fof(m__1709,hypothesis,
( xp = sziznziztdt0(xs)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0) )
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& aVector0(xp) ) ).
fof(m__1726,hypothesis,
( xq = sziznziztdt0(xt)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ) ).
fof(m__1746,hypothesis,
( xA = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(xA) ) ).
fof(m__1766,hypothesis,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ) ).
fof(m__1783,hypothesis,
( xC = sdtasasdt0(xp,xp)
& aScalar0(xC) ) ).
fof(m__1800,hypothesis,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ) ).
fof(m__1837,hypothesis,
( xF = sdtasdt0(xA,xA)
& aScalar0(xF) ) ).
fof(m__1854,hypothesis,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ) ).
fof(m__1892,hypothesis,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ) ).
fof(m__1911,hypothesis,
( xP = sdtasdt0(xE,xH)
& aScalar0(xP) ) ).
fof(m__1930,hypothesis,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ) ).
fof(m__2590,hypothesis,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ).
fof(m__,conjecture,
( sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
& sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ) ).
fof(negated_conjecture,negated_conjecture,
~ ( sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
& sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(c7,plain,
aScalar0(sz0z00),
inference(clausification,[status(esa)],[mSZeroSc]) ).
cnf(c31,plain,
( X1 = X0
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X0) ),
inference(clausification,[status(esa)],[mLEASm]) ).
cnf(c32,plain,
( ~ sdtlseqdt0(X0,X2)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(X2,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| sdtlseqdt0(X0,X1) ),
inference(clausification,[status(esa)],[mLETrn]) ).
cnf(c33,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X3)
| ~ sdtlseqdt0(X3,X2)
| sdtlseqdt0(sdtpldt0(X0,X3),sdtpldt0(X1,X2))
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ sdtlseqdt0(X0,X1) ),
inference(clausification,[status(esa)],[mLEMon]) ).
cnf(c35,plain,
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(clausification,[status(esa)],[mLETot]) ).
cnf(c36,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0) ),
inference(clausification,[status(esa)],[mPosMon]) ).
cnf(c37,plain,
( ~ sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,sdtasdt0(X1,X0))
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,X0) ),
inference(clausification,[status(esa)],[mPosMon]) ).
cnf(c38,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(clausification,[status(esa)],[mSqPos]) ).
cnf(c53,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(clausification,[status(esa)],[mScSqPos]) ).
cnf(c59,plain,
aVector0(xp),
inference(clausification,[status(esa)],[m__1709]) ).
cnf(c63,plain,
aVector0(xq),
inference(clausification,[status(esa)],[m__1726]) ).
cnf(c67,plain,
aScalar0(xA),
inference(clausification,[status(esa)],[m__1746]) ).
cnf(c69,plain,
aScalar0(xB),
inference(clausification,[status(esa)],[m__1766]) ).
cnf(c71,plain,
aScalar0(xC),
inference(clausification,[status(esa)],[m__1783]) ).
cnf(c72,plain,
xC = sdtasasdt0(xp,xp),
inference(clausification,[status(esa)],[m__1783]) ).
cnf(c73,plain,
aScalar0(xD),
inference(clausification,[status(esa)],[m__1800]) ).
cnf(c74,plain,
xD = sdtasasdt0(xq,xq),
inference(clausification,[status(esa)],[m__1800]) ).
cnf(c77,plain,
aScalar0(xF),
inference(clausification,[status(esa)],[m__1837]) ).
cnf(c78,plain,
xF = sdtasdt0(xA,xA),
inference(clausification,[status(esa)],[m__1837]) ).
cnf(c79,plain,
aScalar0(xG),
inference(clausification,[status(esa)],[m__1854]) ).
cnf(c80,plain,
xG = sdtasdt0(xB,xB),
inference(clausification,[status(esa)],[m__1854]) ).
cnf(c83,plain,
aScalar0(xR),
inference(clausification,[status(esa)],[m__1892]) ).
cnf(c84,plain,
xR = sdtasdt0(xC,xG),
inference(clausification,[status(esa)],[m__1892]) ).
cnf(c85,plain,
aScalar0(xP),
inference(clausification,[status(esa)],[m__1911]) ).
cnf(c87,plain,
aScalar0(xS),
inference(clausification,[status(esa)],[m__1930]) ).
cnf(c88,plain,
xS = sdtasdt0(xF,xD),
inference(clausification,[status(esa)],[m__1930]) ).
cnf(c95,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(clausification,[status(esa)],[m__2590]) ).
cnf(c97,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ sdtlseqdt0(sz0z00,xD)
| ~ sdtlseqdt0(sz0z00,xF)
| ~ aScalar0(xD)
| ~ aScalar0(xF)
| sdtlseqdt0(sz0z00,xS) ),
inference(superposition,[status(thm)],[c88,c37]) ).
cnf(d1,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xF)
| ~ sdtlseqdt0(sz0z00,xD)
| ~ aScalar0(xF) ),
inference(resolution,[status(thm)],[c73,d0]) ).
cnf(d2,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xF)
| ~ sdtlseqdt0(sz0z00,xD) ),
inference(resolution,[status(thm)],[c77,d1]) ).
cnf(d3,plain,
( ~ aVector0(xq)
| sdtlseqdt0(sz0z00,xD) ),
inference(superposition,[status(thm)],[c74,c53]) ).
cnf(d4,plain,
sdtlseqdt0(sz0z00,xD),
inference(resolution,[status(thm)],[c63,d3]) ).
cnf(d5,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xF) ),
inference(resolution,[status(thm)],[d4,d2]) ).
cnf(d6,plain,
( ~ aScalar0(xA)
| sdtlseqdt0(sz0z00,xF) ),
inference(superposition,[status(thm)],[c78,c38]) ).
cnf(d7,plain,
sdtlseqdt0(sz0z00,xF),
inference(resolution,[status(thm)],[c67,d6]) ).
cnf(d8,plain,
sdtlseqdt0(sz0z00,xS),
inference(resolution,[status(thm)],[d7,d5]) ).
cnf(d9,plain,
( ~ sdtlseqdt0(X2,X0)
| sdtlseqdt0(X2,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[c35,c32]) ).
cnf(d10,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ aScalar0(xP)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[c36,c97]) ).
cnf(d11,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)) ),
inference(resolution,[status(thm)],[c85,d10]) ).
cnf(d12,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xR)
| ~ aScalar0(xS)
| ~ aScalar0(xR)
| ~ sdtlseqdt0(sz0z00,xP) ),
inference(resolution,[status(thm)],[d11,c36]) ).
cnf(d13,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(sz0z00,xR)
| ~ aScalar0(xS) ),
inference(resolution,[status(thm)],[c83,d12]) ).
cnf(d14,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xP)
| ~ sdtlseqdt0(sz0z00,xR) ),
inference(resolution,[status(thm)],[c87,d13]) ).
cnf(d15,plain,
( ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(sz0z00,xC)
| ~ aScalar0(xG)
| ~ aScalar0(xC)
| sdtlseqdt0(sz0z00,xR) ),
inference(superposition,[status(thm)],[c84,c37]) ).
cnf(d16,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(sz0z00,xC)
| ~ aScalar0(xG) ),
inference(resolution,[status(thm)],[c71,d15]) ).
cnf(d17,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xG)
| ~ sdtlseqdt0(sz0z00,xC) ),
inference(resolution,[status(thm)],[c79,d16]) ).
cnf(d18,plain,
( ~ aVector0(xp)
| sdtlseqdt0(sz0z00,xC) ),
inference(superposition,[status(thm)],[c72,c53]) ).
cnf(d19,plain,
sdtlseqdt0(sz0z00,xC),
inference(resolution,[status(thm)],[c59,d18]) ).
cnf(d20,plain,
( sdtlseqdt0(sz0z00,xR)
| ~ sdtlseqdt0(sz0z00,xG) ),
inference(resolution,[status(thm)],[d19,d17]) ).
cnf(d21,plain,
( ~ aScalar0(xB)
| sdtlseqdt0(sz0z00,xG) ),
inference(superposition,[status(thm)],[c80,c38]) ).
cnf(d22,plain,
sdtlseqdt0(sz0z00,xG),
inference(resolution,[status(thm)],[c69,d21]) ).
cnf(d23,plain,
sdtlseqdt0(sz0z00,xR),
inference(resolution,[status(thm)],[d22,d20]) ).
cnf(d24,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| ~ sdtlseqdt0(sz0z00,xP) ),
inference(resolution,[status(thm)],[d23,d14]) ).
cnf(d25,plain,
~ sdtlseqdt0(sz0z00,xP),
inference(resolution,[status(thm)],[d8,d24]) ).
cnf(d26,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ aScalar0(xP)
| ~ aScalar0(sz0z00) ),
inference(resolution,[status(thm)],[d25,c35]) ).
cnf(d27,plain,
( sdtlseqdt0(xP,sz0z00)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[c7,d26]) ).
cnf(d28,plain,
sdtlseqdt0(xP,sz0z00),
inference(resolution,[status(thm)],[c85,d27]) ).
cnf(d29,plain,
( sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xP,X0)
| ~ aScalar0(sz0z00)
| ~ aScalar0(X0)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[d28,d9]) ).
cnf(d30,plain,
( sdtlseqdt0(xP,X0)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(xP)
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[c7,d29]) ).
cnf(d31,plain,
( sdtlseqdt0(xP,X0)
| sdtlseqdt0(X0,sz0z00)
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[c85,d30]) ).
cnf(d32,plain,
( ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0)
| ~ aScalar0(sz0z00)
| X0 = sz0z00
| sdtlseqdt0(xP,X0)
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[d31,c31]) ).
cnf(d33,plain,
( sdtlseqdt0(xP,X0)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0)
| X0 = sz0z00 ),
inference(resolution,[status(thm)],[c7,d32]) ).
cnf(d34,plain,
( sdtlseqdt0(xP,xS)
| ~ aScalar0(xS)
| xS = sz0z00 ),
inference(resolution,[status(thm)],[d33,d8]) ).
cnf(d35,plain,
( sdtlseqdt0(xP,xS)
| xS = sz0z00 ),
inference(resolution,[status(thm)],[c87,d34]) ).
cnf(d36,plain,
( sdtlseqdt0(xP,xR)
| ~ aScalar0(xR)
| xR = sz0z00 ),
inference(resolution,[status(thm)],[d33,d23]) ).
cnf(d37,plain,
( sdtlseqdt0(xP,xR)
| xR = sz0z00 ),
inference(resolution,[status(thm)],[c83,d36]) ).
cnf(d38,plain,
( ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,xR)
| ~ aScalar0(xP)
| ~ aScalar0(xS)
| ~ aScalar0(xP)
| ~ aScalar0(xR) ),
inference(resolution,[status(thm)],[c95,c33]) ).
cnf(d39,plain,
( ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,xR)
| ~ aScalar0(xS)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[c83,d38]) ).
cnf(d40,plain,
( ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,xR)
| ~ aScalar0(xS) ),
inference(resolution,[status(thm)],[c85,d39]) ).
cnf(d41,plain,
( ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,xR) ),
inference(resolution,[status(thm)],[c87,d40]) ).
cnf(d42,plain,
( ~ sdtlseqdt0(xP,xR)
| xS = sz0z00 ),
inference(resolution,[status(thm)],[d35,d41]) ).
cnf(d43,plain,
( xR = sz0z00
| xS = sz0z00 ),
inference(resolution,[status(thm)],[d42,d37]) ).
cnf(d44,plain,
( xR = sz0z00
| ~ sdtlseqdt0(xP,xR)
| ~ sdtlseqdt0(xP,sz0z00) ),
inference(superposition,[status(thm)],[d43,d41]) ).
cnf(d45,plain,
( ~ sdtlseqdt0(xP,xR)
| xR = sz0z00 ),
inference(resolution,[status(thm)],[d28,d44]) ).
cnf(d46,plain,
( xR = sz0z00
| xR = sz0z00 ),
inference(resolution,[status(thm)],[d45,d37]) ).
cnf(d47,plain,
( ~ sdtlseqdt0(xP,xS)
| ~ sdtlseqdt0(xP,sz0z00) ),
inference(demodulation,[status(thm)],[d41,d46]) ).
cnf(d48,plain,
~ sdtlseqdt0(xP,xS),
inference(resolution,[status(thm)],[d28,d47]) ).
cnf(d49,plain,
xS = sz0z00,
inference(resolution,[status(thm)],[d48,d35]) ).
cnf(d50,plain,
~ sdtlseqdt0(xP,sz0z00),
inference(demodulation,[status(thm)],[d48,d49]) ).
cnf(d51,plain,
$false,
inference(resolution,[status(thm)],[d28,d50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : RNG071+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sat Sep 26 05:57:35 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.73/3.07 % SZS status Theorem for theBenchmark.p
% 5.73/3.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------