%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : RNG049+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:42 AM UTC 2026
% Result : Theorem 33.07s 32.05s
% Output : CNFRefutation 33.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 14
% Syntax : Number of formulae : 55 ( 17 unt; 0 def)
% Number of atoms : 143 ( 27 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 150 ( 62 ~; 51 |; 20 &)
% ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 35 ( 0 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSuccNat,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( szszuzczcdt0(X0) != sz00
& aNaturalNumber0(szszuzczcdt0(X0)) ) ) ).
fof(mIH,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> iLess0(X0,szszuzczcdt0(X0)) ) ).
fof(mMulSc,axiom,
! [X0,X1] :
( ( aScalar0(X1)
& aScalar0(X0) )
=> aScalar0(sdtasdt0(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(mDimNat,axiom,
! [X0] :
( aVector0(X0)
=> aNaturalNumber0(aDimensionOf0(X0)) ) ).
fof(mElmSc,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X1)
& aVector0(X0) )
=> aScalar0(sdtlbdtrb0(X0,X1)) ) ).
fof(mScPr,axiom,
! [X0,X1] :
( ( aVector0(X1)
& aVector0(X0) )
=> ( aDimensionOf0(X0) = aDimensionOf0(X1)
=> aScalar0(sdtasasdt0(X0,X1)) ) ) ).
fof(mDefSPN,axiom,
! [X0,X1] :
( ( aVector0(X1)
& aVector0(X0) )
=> ( ( aDimensionOf0(X1) != sz00
& aDimensionOf0(X0) = aDimensionOf0(X1) )
=> sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1)))) ) ) ).
fof(m__1542,hypothesis,
aVector0(xs) ).
fof(m__1516,hypothesis,
! [X0] :
( aVector0(X0)
=> ( iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ) ) ).
fof(m__1542_01,hypothesis,
aDimensionOf0(xs) != sz00 ).
fof(m__1568,hypothesis,
( ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(sziznziztdt0(xs),X0) = sdtlbdtrb0(xs,X0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(sziznziztdt0(xs),X0) = sdtlbdtrb0(xs,X0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ) ).
fof(m__1590,hypothesis,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(sziznziztdt0(xs),X0) = sdtlbdtrb0(xs,X0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(sziznziztdt0(xs),X0) = sdtlbdtrb0(xs,X0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ) ).
fof(m__,conjecture,
sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ).
fof(negated_conjecture,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(c1,plain,
( aNaturalNumber0(szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mSuccNat]) ).
cnf(c6,plain,
( iLess0(X0,szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[mIH]) ).
cnf(c9,plain,
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(clausification,[status(esa)],[mMulSc]) ).
cnf(c36,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0) ),
inference(clausification,[status(esa)],[mPosMon]) ).
cnf(c40,plain,
( aNaturalNumber0(aDimensionOf0(X0))
| ~ aVector0(X0) ),
inference(clausification,[status(esa)],[mDimNat]) ).
cnf(c41,plain,
( aScalar0(sdtlbdtrb0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aVector0(X0) ),
inference(clausification,[status(esa)],[mElmSc]) ).
cnf(c50,plain,
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(clausification,[status(esa)],[mScPr]) ).
cnf(c52,plain,
( ~ aVector0(X0)
| ~ aVector0(X1)
| sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(X0) != aDimensionOf0(X1) ),
inference(clausification,[status(esa)],[mDefSPN]) ).
cnf(c53,plain,
aVector0(xs),
inference(clausification,[status(esa)],[m__1542]) ).
cnf(c54,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| ~ aVector0(X0) ),
inference(clausification,[status(esa)],[m__1516]) ).
cnf(c55,plain,
aDimensionOf0(xs) != sz00,
inference(clausification,[status(esa)],[m__1542_01]) ).
cnf(c56,plain,
aVector0(sziznziztdt0(xs)),
inference(clausification,[status(esa)],[m__1568]) ).
cnf(c57,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(clausification,[status(esa)],[m__1568]) ).
cnf(c58,plain,
( sdtlbdtrb0(sziznziztdt0(xs),X0) = sdtlbdtrb0(xs,X0)
| ~ aNaturalNumber0(X0) ),
inference(clausification,[status(esa)],[m__1568]) ).
cnf(c68,plain,
sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(clausification,[status(esa)],[m__1590]) ).
cnf(c69,plain,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ aVector0(X0)
| ~ aVector0(X0)
| aScalar0(sdtasasdt0(X0,X0)) ),
inference(equality_resolution,[status(thm)],[c50]) ).
cnf(d1,plain,
( ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs)))
| iLess0(aDimensionOf0(sziznziztdt0(xs)),aDimensionOf0(xs)) ),
inference(superposition,[status(thm)],[c57,c6]) ).
cnf(d2,plain,
( ~ aVector0(sziznziztdt0(xs))
| sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[d1,c54]) ).
cnf(d3,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[c56,d2]) ).
cnf(d4,plain,
( ~ aVector0(X0)
| ~ aVector0(X0)
| sdtasasdt0(X0,X0) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X0)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X0,aDimensionOf0(X0))))
| aDimensionOf0(X0) = sz00 ),
inference(equality_resolution,[status(thm)],[c52]) ).
cnf(d5,plain,
( sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(xs) = sz00 ),
inference(resolution,[status(thm)],[d4,c53]) ).
cnf(d6,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(resolution,[status(thm)],[c55,d5]) ).
cnf(d7,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(superposition,[status(thm)],[d6,c36]) ).
cnf(d8,plain,
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(resolution,[status(thm)],[c69,d7]) ).
cnf(d9,plain,
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(resolution,[status(thm)],[c68,d8]) ).
cnf(d10,plain,
( ~ aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))
| ~ aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[d9,c9]) ).
cnf(d11,plain,
( ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs)))
| aNaturalNumber0(aDimensionOf0(xs)) ),
inference(superposition,[status(thm)],[c57,c1]) ).
cnf(d12,plain,
( ~ aVector0(sziznziztdt0(xs))
| aNaturalNumber0(aDimensionOf0(xs)) ),
inference(resolution,[status(thm)],[d11,c40]) ).
cnf(d13,plain,
aNaturalNumber0(aDimensionOf0(xs)),
inference(resolution,[status(thm)],[c56,d12]) ).
cnf(d14,plain,
sdtlbdtrb0(sziznziztdt0(xs),aDimensionOf0(xs)) = sdtlbdtrb0(xs,aDimensionOf0(xs)),
inference(resolution,[status(thm)],[c58,d13]) ).
cnf(d15,plain,
( ~ aVector0(sziznziztdt0(xs))
| ~ aNaturalNumber0(aDimensionOf0(xs))
| aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs))) ),
inference(superposition,[status(thm)],[d14,c41]) ).
cnf(d16,plain,
( aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))
| ~ aNaturalNumber0(aDimensionOf0(xs)) ),
inference(resolution,[status(thm)],[c56,d15]) ).
cnf(d17,plain,
aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs))),
inference(resolution,[status(thm)],[d13,d16]) ).
cnf(d18,plain,
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[d17,d10]) ).
cnf(d19,plain,
( ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs)))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[d18,d3]) ).
cnf(d20,plain,
( ~ aVector0(sziznziztdt0(xs))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[d19,d0]) ).
cnf(d21,plain,
~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))),
inference(resolution,[status(thm)],[c56,d20]) ).
cnf(d22,plain,
~ aVector0(sziznziztdt0(xs)),
inference(resolution,[status(thm)],[d21,c40]) ).
cnf(d23,plain,
$false,
inference(resolution,[status(thm)],[c56,d22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG049+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n004.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 05:52:07 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.07/32.05 % SZS status Theorem for theBenchmark.p
% 33.07/32.05 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------