%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG081+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 : Tue Sep 29 12:35:58 PM UTC 2026
% Result : Theorem 0.37s 0.48s
% Output : Refutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 108 ( 18 unt; 9 def)
% Number of atoms : 464 ( 122 equ)
% Maximal formula atoms : 40 ( 4 avg)
% Number of connectives : 547 ( 191 ~; 178 |; 150 &)
% ( 9 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 113 ( 0 sgn 57 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEMonM) ).
fof(f34,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( aDimensionOf0(X0) = aDimensionOf0(X1)
=> aScalar0(sdtasasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScPr) ).
fof(f35,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( ( aDimensionOf0(X0) = aDimensionOf0(X1)
& aDimensionOf0(X1) = sz00 )
=> sdtasasdt0(X0,X1) = sz0z00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSPZ) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScSqPos) ).
fof(f38,axiom,
( aVector0(xs)
& aVector0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678) ).
fof(f40,axiom,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678_01) ).
fof(f41,conjecture,
( ( aDimensionOf0(xs) != sz00
=> ? [X0] :
( aVector0(X0)
& szszuzczcdt0(aDimensionOf0(X0)) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(X0,X1) = sdtlbdtrb0(xs,X1) )
& X0 = sziznziztdt0(xs)
& ? [X1] :
( aVector0(X1)
& szszuzczcdt0(aDimensionOf0(X1)) = aDimensionOf0(xt)
& ! [X2] :
( aNaturalNumber0(X2)
=> sdtlbdtrb0(X1,X2) = sdtlbdtrb0(xt,X2) )
& X1 = sziznziztdt0(xt)
& ? [X2] :
( aScalar0(X2)
& X2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& ? [X3] :
( aScalar0(X3)
& X3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& ? [X4] :
( aScalar0(X4)
& X4 = sdtasasdt0(X0,X0)
& ? [X5] :
( aScalar0(X5)
& X5 = sdtasasdt0(X1,X1)
& ? [X6] :
( aScalar0(X6)
& X6 = sdtasasdt0(X0,X1)
& ? [X7] :
( aScalar0(X7)
& X7 = sdtasdt0(X2,X2)
& ? [X8] :
( aScalar0(X8)
& X8 = sdtasdt0(X3,X3)
& ? [X9] :
( aScalar0(X9)
& X9 = sdtasdt0(X2,X3)
& ? [X10] :
( aScalar0(X10)
& X10 = sdtasdt0(X4,X8)
& ? [X11] :
( aScalar0(X11)
& X11 = sdtasdt0(X6,X9)
& ? [X12] :
( aScalar0(X12)
& X12 = sdtasdt0(X7,X5)
& ? [X13] :
( aScalar0(X13)
& X13 = sdtasdt0(X10,X12)
& sdtlseqdt0(sdtasdt0(X6,X6),sdtasdt0(X4,X5))
& sdtlseqdt0(sdtpldt0(X11,X11),sdtpldt0(X10,X12))
& sdtlseqdt0(sdtasdt0(sdtpldt0(X6,X9),sdtpldt0(X6,X9)),sdtasdt0(sdtpldt0(X4,X7),sdtpldt0(X5,X8)))
& sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f42,negated_conjecture,
~ ( ( aDimensionOf0(xs) != sz00
=> ? [X0] :
( aVector0(X0)
& szszuzczcdt0(aDimensionOf0(X0)) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(X0,X1) = sdtlbdtrb0(xs,X1) )
& X0 = sziznziztdt0(xs)
& ? [X1] :
( aVector0(X1)
& szszuzczcdt0(aDimensionOf0(X1)) = aDimensionOf0(xt)
& ! [X2] :
( aNaturalNumber0(X2)
=> sdtlbdtrb0(X1,X2) = sdtlbdtrb0(xt,X2) )
& X1 = sziznziztdt0(xt)
& ? [X2] :
( aScalar0(X2)
& X2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& ? [X3] :
( aScalar0(X3)
& X3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& ? [X4] :
( aScalar0(X4)
& X4 = sdtasasdt0(X0,X0)
& ? [X5] :
( aScalar0(X5)
& X5 = sdtasasdt0(X1,X1)
& ? [X6] :
( aScalar0(X6)
& X6 = sdtasasdt0(X0,X1)
& ? [X7] :
( aScalar0(X7)
& X7 = sdtasdt0(X2,X2)
& ? [X8] :
( aScalar0(X8)
& X8 = sdtasdt0(X3,X3)
& ? [X9] :
( aScalar0(X9)
& X9 = sdtasdt0(X2,X3)
& ? [X10] :
( aScalar0(X10)
& X10 = sdtasdt0(X4,X8)
& ? [X11] :
( aScalar0(X11)
& X11 = sdtasdt0(X6,X9)
& ? [X12] :
( aScalar0(X12)
& X12 = sdtasdt0(X7,X5)
& ? [X13] :
( aScalar0(X13)
& X13 = sdtasdt0(X10,X12)
& sdtlseqdt0(sdtasdt0(X6,X6),sdtasdt0(X4,X5))
& sdtlseqdt0(sdtpldt0(X11,X11),sdtpldt0(X10,X12))
& sdtlseqdt0(sdtasdt0(sdtpldt0(X6,X9),sdtpldt0(X6,X9)),sdtasdt0(sdtpldt0(X4,X7),sdtpldt0(X5,X8)))
& sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
~ ( ( aDimensionOf0(xs) != sz00
=> ? [X0] :
( aVector0(X0)
& szszuzczcdt0(aDimensionOf0(X0)) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(X0,X1) = sdtlbdtrb0(xs,X1) )
& X0 = sziznziztdt0(xs)
& ? [X2] :
( aVector0(X2)
& aDimensionOf0(xt) = szszuzczcdt0(aDimensionOf0(X2))
& ! [X3] :
( aNaturalNumber0(X3)
=> sdtlbdtrb0(X2,X3) = sdtlbdtrb0(xt,X3) )
& sziznziztdt0(xt) = X2
& ? [X4] :
( aScalar0(X4)
& sdtlbdtrb0(xs,aDimensionOf0(xs)) = X4
& ? [X5] :
( aScalar0(X5)
& sdtlbdtrb0(xt,aDimensionOf0(xt)) = X5
& ? [X6] :
( aScalar0(X6)
& sdtasasdt0(X0,X0) = X6
& ? [X7] :
( aScalar0(X7)
& sdtasasdt0(X2,X2) = X7
& ? [X8] :
( aScalar0(X8)
& sdtasasdt0(X0,X2) = X8
& ? [X9] :
( aScalar0(X9)
& sdtasdt0(X4,X4) = X9
& ? [X10] :
( aScalar0(X10)
& sdtasdt0(X5,X5) = X10
& ? [X11] :
( aScalar0(X11)
& sdtasdt0(X4,X5) = X11
& ? [X12] :
( aScalar0(X12)
& sdtasdt0(X6,X10) = X12
& ? [X13] :
( aScalar0(X13)
& sdtasdt0(X8,X11) = X13
& ? [X14] :
( aScalar0(X14)
& sdtasdt0(X9,X7) = X14
& ? [X15] :
( aScalar0(X15)
& sdtasdt0(X12,X14) = X15
& sdtlseqdt0(sdtasdt0(X8,X8),sdtasdt0(X6,X7))
& sdtlseqdt0(sdtpldt0(X13,X13),sdtpldt0(X12,X14))
& sdtlseqdt0(sdtasdt0(sdtpldt0(X8,X11),sdtpldt0(X8,X11)),sdtasdt0(sdtpldt0(X6,X9),sdtpldt0(X7,X10)))
& sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(rectify,[],[f42]) ).
fof(f79,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f80,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(flattening,[],[f79]) ).
fof(f96,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f97,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sz0z00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f99,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sz0z00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f98]) ).
fof(f102,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f105,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& ( ? [X0] :
( aVector0(X0)
& szszuzczcdt0(aDimensionOf0(X0)) = aDimensionOf0(xs)
& ! [X1] :
( sdtlbdtrb0(X0,X1) = sdtlbdtrb0(xs,X1)
| ~ aNaturalNumber0(X1) )
& X0 = sziznziztdt0(xs)
& ? [X2] :
( aVector0(X2)
& aDimensionOf0(xt) = szszuzczcdt0(aDimensionOf0(X2))
& ! [X3] :
( sdtlbdtrb0(X2,X3) = sdtlbdtrb0(xt,X3)
| ~ aNaturalNumber0(X3) )
& sziznziztdt0(xt) = X2
& ? [X4] :
( aScalar0(X4)
& sdtlbdtrb0(xs,aDimensionOf0(xs)) = X4
& ? [X5] :
( aScalar0(X5)
& sdtlbdtrb0(xt,aDimensionOf0(xt)) = X5
& ? [X6] :
( aScalar0(X6)
& sdtasasdt0(X0,X0) = X6
& ? [X7] :
( aScalar0(X7)
& sdtasasdt0(X2,X2) = X7
& ? [X8] :
( aScalar0(X8)
& sdtasasdt0(X0,X2) = X8
& ? [X9] :
( aScalar0(X9)
& sdtasdt0(X4,X4) = X9
& ? [X10] :
( aScalar0(X10)
& sdtasdt0(X5,X5) = X10
& ? [X11] :
( aScalar0(X11)
& sdtasdt0(X4,X5) = X11
& ? [X12] :
( aScalar0(X12)
& sdtasdt0(X6,X10) = X12
& ? [X13] :
( aScalar0(X13)
& sdtasdt0(X8,X11) = X13
& ? [X14] :
( aScalar0(X14)
& sdtasdt0(X9,X7) = X14
& ? [X15] :
( aScalar0(X15)
& sdtasdt0(X12,X14) = X15
& sdtlseqdt0(sdtasdt0(X8,X8),sdtasdt0(X6,X7))
& sdtlseqdt0(sdtpldt0(X13,X13),sdtpldt0(X12,X14))
& sdtlseqdt0(sdtasdt0(sdtpldt0(X8,X11),sdtpldt0(X8,X11)),sdtasdt0(sdtpldt0(X6,X9),sdtpldt0(X7,X10)))
& sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| sz00 = aDimensionOf0(xs) ) ),
inference(ennf_transformation,[],[f43]) ).
fof(f139,plain,
! [X2,X3,X0,X1] :
( ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f153,plain,
! [X0,X1] :
( ~ aVector0(X1)
| ~ aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| aScalar0(sdtasasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f97]) ).
fof(f154,plain,
! [X0,X1] :
( sz00 != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz0z00 = sdtasasdt0(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f156,plain,
! [X0] :
( ~ aVector0(X0)
| sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f157,plain,
aVector0(xt),
inference(cnf_transformation,[],[f38]) ).
fof(f158,plain,
aVector0(xs),
inference(cnf_transformation,[],[f38]) ).
fof(f160,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[],[f40]) ).
fof(f161,plain,
( sz00 = aDimensionOf0(xs)
| sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(cnf_transformation,[],[f105]) ).
fof(f197,plain,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(cnf_transformation,[],[f105]) ).
fof(f234,plain,
! [X2,X3,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X2,X3)
| sdtlseqdt0(sz0z00,X2)
| sdtlseqdt0(X0,X1)
| aScalar0(X3) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f244,plain,
! [X0,X1] :
( ~ aVector0(X0)
| ~ aVector0(X1)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aScalar0(sdtasasdt0(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f245,plain,
! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f247,plain,
sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f265,plain,
( sz00 = aDimensionOf0(xs)
| ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f267,definition,
( spl16_1
<=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f268,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl16_2
<=> sz00 = aDimensionOf0(xs) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f273,plain,
( sz00 = aDimensionOf0(xs)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( ~ spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f265,f271,f267]) ).
fof(f448,plain,
spl16_1,
inference(avatar_split_clause,[],[f247,f267]) ).
fof(f467,plain,
( sz00 = aDimensionOf0(xt)
| ~ spl16_2 ),
inference(forward_demodulation,[],[f160,f273]) ).
fof(f606,plain,
! [X0] :
( ~ aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(xt)
| ~ aScalar0(sdtasasdt0(xt,X0)) ),
inference(resolution,[],[f244,f157]) ).
fof(f607,plain,
! [X0] :
( ~ aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aScalar0(sdtasasdt0(xs,X0)) ),
inference(resolution,[],[f244,f158]) ).
fof(f609,plain,
( ! [X0] :
( sz00 != aDimensionOf0(X0)
| ~ aVector0(X0)
| ~ aScalar0(sdtasasdt0(xs,X0)) )
| ~ spl16_2 ),
inference(forward_demodulation,[],[f607,f273]) ).
fof(f610,plain,
( ! [X0] :
( sz00 != aDimensionOf0(X0)
| ~ aVector0(X0)
| ~ aScalar0(sdtasasdt0(xt,X0)) )
| ~ spl16_2 ),
inference(forward_demodulation,[],[f606,f467]) ).
fof(f626,definition,
( spl16_46
<=> aScalar0(sdtasasdt0(xt,xt)) ),
introduced(definition,[new_symbols(definition,[spl16_46])],[avatar_definition]) ).
fof(f630,definition,
( spl16_47
<=> aScalar0(sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[spl16_47])],[avatar_definition]) ).
fof(f697,plain,
( ! [X0] :
( sz00 != sz00
| ~ aVector0(X0)
| ~ aVector0(xt)
| sz00 != aDimensionOf0(X0)
| sz0z00 = sdtasasdt0(X0,xt) )
| ~ spl16_2 ),
inference(superposition,[],[f154,f467]) ).
fof(f698,plain,
( ! [X0] :
( ~ aVector0(X0)
| ~ aVector0(xt)
| sz00 != aDimensionOf0(X0)
| sz0z00 = sdtasasdt0(X0,xt) )
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f697]) ).
fof(f700,plain,
( ! [X0] :
( sz00 != aDimensionOf0(X0)
| ~ aVector0(X0)
| sz0z00 = sdtasasdt0(X0,xt) )
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f698,f157]) ).
fof(f756,definition,
( spl16_48
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl16_48])],[avatar_definition]) ).
fof(f777,plain,
( sz00 != sz00
| ~ aVector0(xs)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl16_2 ),
inference(superposition,[],[f609,f273]) ).
fof(f778,plain,
( sz00 != sz00
| ~ aVector0(xt)
| ~ aScalar0(sdtasasdt0(xs,xt))
| ~ spl16_2 ),
inference(superposition,[],[f609,f467]) ).
fof(f779,plain,
( ~ aVector0(xt)
| ~ aScalar0(sdtasasdt0(xs,xt))
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f778]) ).
fof(f780,plain,
( ~ aVector0(xs)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f777]) ).
fof(f781,plain,
( ~ aScalar0(sdtasasdt0(xs,xt))
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f779,f157]) ).
fof(f782,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f780,f158]) ).
fof(f785,plain,
( ~ spl16_47
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f782,f271,f630]) ).
fof(f787,plain,
( aScalar0(sdtasasdt0(xs,xt))
| aScalar0(sdtasasdt0(xs,xs))
| aScalar0(sdtasasdt0(xs,xt))
| sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt))
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt))
| sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs))
| aScalar0(sdtasasdt0(xt,xt))
| ~ spl16_1 ),
inference(resolution,[],[f234,f268]) ).
fof(f794,plain,
( aScalar0(sdtasasdt0(xs,xt))
| aScalar0(sdtasasdt0(xs,xs))
| sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt))
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt))
| sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs))
| aScalar0(sdtasasdt0(xt,xt))
| ~ spl16_1 ),
inference(duplicate_literal_removal,[],[f787]) ).
fof(f799,definition,
( spl16_50
<=> sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[spl16_50])],[avatar_definition]) ).
fof(f801,plain,
( sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs))
| ~ spl16_50 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f803,definition,
( spl16_51
<=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt)) ),
introduced(definition,[new_symbols(definition,[spl16_51])],[avatar_definition]) ).
fof(f805,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt))
| ~ spl16_51 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f807,definition,
( spl16_52
<=> sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt)) ),
introduced(definition,[new_symbols(definition,[spl16_52])],[avatar_definition]) ).
fof(f809,plain,
( sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt))
| ~ spl16_52 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f811,definition,
( spl16_53
<=> aScalar0(sdtasasdt0(xs,xt)) ),
introduced(definition,[new_symbols(definition,[spl16_53])],[avatar_definition]) ).
fof(f814,plain,
( spl16_46
| spl16_50
| spl16_51
| spl16_52
| spl16_47
| spl16_53
| ~ spl16_1 ),
inference(avatar_split_clause,[],[f794,f267,f811,f630,f807,f803,f799,f626]) ).
fof(f857,plain,
( ~ spl16_53
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f781,f271,f811]) ).
fof(f994,plain,
( sz00 != sz00
| ~ aVector0(xt)
| ~ aScalar0(sdtasasdt0(xt,xt))
| ~ spl16_2 ),
inference(superposition,[],[f610,f467]) ).
fof(f995,plain,
( ~ aVector0(xt)
| ~ aScalar0(sdtasasdt0(xt,xt))
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f994]) ).
fof(f997,plain,
( ~ aScalar0(sdtasasdt0(xt,xt))
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f995,f157]) ).
fof(f1001,plain,
( ~ spl16_46
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f997,f271,f626]) ).
fof(f1002,plain,
( sz00 != sz00
| ~ aVector0(xs)
| sz0z00 = sdtasasdt0(xs,xt)
| ~ spl16_2 ),
inference(superposition,[],[f700,f273]) ).
fof(f1003,plain,
( sz00 != sz00
| ~ aVector0(xt)
| sz0z00 = sdtasasdt0(xt,xt)
| ~ spl16_2 ),
inference(superposition,[],[f700,f467]) ).
fof(f1004,plain,
( ~ aVector0(xt)
| sz0z00 = sdtasasdt0(xt,xt)
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f1003]) ).
fof(f1005,plain,
( ~ aVector0(xs)
| sz0z00 = sdtasasdt0(xs,xt)
| ~ spl16_2 ),
inference(trivial_inequality_removal,[],[f1002]) ).
fof(f1006,plain,
( sz0z00 = sdtasasdt0(xt,xt)
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f1004,f157]) ).
fof(f1007,plain,
( sz0z00 = sdtasasdt0(xs,xt)
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f1005,f158]) ).
fof(f1088,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ aVector0(xt)
| ~ spl16_2 ),
inference(superposition,[],[f245,f1006]) ).
fof(f1093,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f1088,f157]) ).
fof(f1097,plain,
( ~ spl16_48
| ~ spl16_2 ),
inference(avatar_split_clause,[],[f1093,f271,f756]) ).
fof(f1132,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl16_2
| ~ spl16_51 ),
inference(superposition,[],[f805,f1007]) ).
fof(f1142,plain,
( spl16_48
| ~ spl16_2
| ~ spl16_51 ),
inference(avatar_split_clause,[],[f1132,f803,f271,f756]) ).
fof(f1154,plain,
( sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))
| ~ spl16_2
| ~ spl16_50 ),
inference(forward_demodulation,[],[f801,f1007]) ).
fof(f1167,plain,
( ~ aVector0(xs)
| ~ spl16_2
| ~ spl16_50 ),
inference(resolution,[],[f1154,f245]) ).
fof(f1172,plain,
( $false
| ~ spl16_2
| ~ spl16_50 ),
inference(forward_subsumption_resolution,[],[f1167,f158]) ).
fof(f1173,plain,
( ~ spl16_2
| ~ spl16_50 ),
inference(avatar_contradiction_clause,[],[f1172]) ).
fof(f1177,plain,
( sdtlseqdt0(sdtasasdt0(xs,xt),sz0z00)
| ~ spl16_2
| ~ spl16_52 ),
inference(forward_demodulation,[],[f809,f1006]) ).
fof(f1178,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl16_2
| ~ spl16_52 ),
inference(forward_demodulation,[],[f1177,f1007]) ).
fof(f1179,plain,
( spl16_48
| ~ spl16_2
| ~ spl16_52 ),
inference(avatar_split_clause,[],[f1178,f807,f271,f756]) ).
cnf(s1,plain,
( ~ spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f274]) ).
cnf(s37,plain,
spl16_1,
inference(sat_conversion,[],[f448]) ).
cnf(s48,plain,
( ~ spl16_2
| ~ spl16_47 ),
inference(sat_conversion,[],[f785]) ).
cnf(s49,plain,
( ~ spl16_1
| spl16_46
| spl16_47
| spl16_50
| spl16_51
| spl16_52
| spl16_53 ),
inference(sat_conversion,[],[f814]) ).
cnf(s50,plain,
( ~ spl16_2
| ~ spl16_53 ),
inference(sat_conversion,[],[f857]) ).
cnf(s54,plain,
( ~ spl16_2
| ~ spl16_46 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s55,plain,
( ~ spl16_2
| ~ spl16_48 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s57,plain,
( ~ spl16_2
| spl16_48
| ~ spl16_51 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s60,plain,
( ~ spl16_2
| ~ spl16_50 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s61,plain,
( ~ spl16_2
| spl16_48
| ~ spl16_52 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s65,plain,
spl16_2,
inference(rat,[],[s1,s37]) ).
cnf(s66,plain,
~ spl16_50,
inference(rat,[],[s60,s65]) ).
cnf(s67,plain,
~ spl16_48,
inference(rat,[],[s55,s65]) ).
cnf(s68,plain,
~ spl16_46,
inference(rat,[],[s54,s65]) ).
cnf(s69,plain,
~ spl16_53,
inference(rat,[],[s50,s65]) ).
cnf(s70,plain,
~ spl16_47,
inference(rat,[],[s48,s65]) ).
cnf(s72,plain,
~ spl16_52,
inference(rat,[],[s61,s65,s67]) ).
cnf(s73,plain,
~ spl16_51,
inference(rat,[],[s57,s65,s67]) ).
cnf(s75,plain,
$false,
inference(rat,[],[s49,s69,s72,s73,s66,s37,s70,s68]) ).
fof(f1180,plain,
$false,
inference(avatar_sat_refutation,[],[s75]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG081+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 23:10:10 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 Running first-order model finding
% 0.12/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.48 % (3437676)Will run a generic schedule for satisfiability detection.
% 0.37/0.48 % (3437683)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1736048187:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.37/0.48 % (3437682)% WARNING: option uhcvi not known.
% 0.37/0.48 % (3437681)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1321189430_2999 on theBenchmark for (2999ds/0Mi)
% 0.37/0.48 % (3437685)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1808071833:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.37/0.48 % (3437684)dis+10_1_sil=32000:sp=arity:random_seed=495718591:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.37/0.48 % (3437686)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3072169979:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.37/0.48 % (3437687)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4098564474:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.37/0.48 % (3437682)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1007901147:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.37/0.48 % TRYING [1]
% 0.37/0.48 % TRYING [2]
% 0.37/0.48 % (3437682) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3437676-3437682"...
% 0.37/0.48 % TRYING [3]
% 0.37/0.48 % (3437682)...printing done.
% 0.37/0.48 % (3437682)Refutation found. Thanks to Tanya!
% 0.37/0.48 % SZS status Theorem for theBenchmark
% 0.37/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.37/0.48 % (3437682)------------------------------
% 0.37/0.48 % (3437682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.37/0.48 % (3437682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.37/0.48 % (3437682)CaDiCaL version: 2.1.3
% 0.37/0.48 % (3437682)Termination reason: Refutation
% 0.37/0.48 % (3437682)Time elapsed: 0.026 s
% 0.37/0.48 % (3437682)Peak memory usage: 13 MB
% 0.37/0.48 % (3437682)Instructions burned: 40 (million)
% 0.37/0.48 % (3437676)Success in time 0.064 s
% 0.37/0.48 % Vampire exiting
%------------------------------------------------------------------------------