%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG052+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 : n005.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:52 PM UTC 2026
% Result : Theorem 5.49s 1.28s
% Output : Refutation 5.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of formulae : 89 ( 35 unt; 2 def)
% Number of atoms : 203 ( 75 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 189 ( 75 ~; 80 |; 22 &)
% ( 2 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 44 ( 0 sgn 41 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00 )
=> ? [X1] :
( aNaturalNumber0(X1)
& X0 = szszuzczcdt0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNatExtr) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( szszuzczcdt0(X0) = szszuzczcdt0(X1)
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSuccEqu) ).
fof(f7,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> iLess0(X0,szszuzczcdt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIH) ).
fof(f30,axiom,
! [X0] :
( aVector0(X0)
=> aNaturalNumber0(aDimensionOf0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDimNat) ).
fof(f38,axiom,
( aVector0(xs)
& aVector0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678) ).
fof(f39,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( aDimensionOf0(X0) = aDimensionOf0(X1)
=> ( iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1652) ).
fof(f40,axiom,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1678_01) ).
fof(f41,axiom,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1692) ).
fof(f42,axiom,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0) )
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1709) ).
fof(f43,axiom,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0) )
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1726) ).
fof(f46,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1783) ).
fof(f47,axiom,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1800) ).
fof(f48,axiom,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1820) ).
fof(f56,conjecture,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f57,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f58,plain,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(flattening,[],[f57]) ).
fof(f61,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& X0 = szszuzczcdt0(X1) )
| ~ aNaturalNumber0(X0)
| sz00 = X0 ),
inference(ennf_transformation,[],[f4]) ).
fof(f62,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& X0 = szszuzczcdt0(X1) )
| ~ aNaturalNumber0(X0)
| sz00 = X0 ),
inference(flattening,[],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( X0 = X1
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f64,plain,
! [X0,X1] :
( X0 = X1
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f63]) ).
fof(f67,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f104,plain,
! [X0] :
( aNaturalNumber0(aDimensionOf0(X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f118,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1)))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f39]) ).
fof(f119,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1)))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f118]) ).
fof(f120,plain,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0)
| ~ aNaturalNumber0(X0) )
& xp = sziznziztdt0(xs) ),
inference(ennf_transformation,[],[f42]) ).
fof(f121,plain,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0)
| ~ aNaturalNumber0(X0) )
& xq = sziznziztdt0(xt) ),
inference(ennf_transformation,[],[f43]) ).
fof(f125,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| szszuzczcdt0(sK0(X0)) = X0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f126,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| aNaturalNumber0(sK0(X0)) ),
inference(cnf_transformation,[],[f62]) ).
fof(f127,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f64]) ).
fof(f128,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| iLess0(X0,szszuzczcdt0(X0)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f161,plain,
! [X0] :
( ~ aVector0(X0)
| aNaturalNumber0(aDimensionOf0(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f174,plain,
aVector0(xs),
inference(cnf_transformation,[],[f38]) ).
fof(f175,plain,
! [X0,X1] :
( ~ aVector0(X1)
| ~ aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1))) ),
inference(cnf_transformation,[],[f119]) ).
fof(f176,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[],[f40]) ).
fof(f177,plain,
sz00 != aDimensionOf0(xs),
inference(cnf_transformation,[],[f41]) ).
fof(f180,plain,
aDimensionOf0(xs) = szszuzczcdt0(aDimensionOf0(xp)),
inference(cnf_transformation,[],[f120]) ).
fof(f181,plain,
aVector0(xp),
inference(cnf_transformation,[],[f120]) ).
fof(f184,plain,
aDimensionOf0(xt) = szszuzczcdt0(aDimensionOf0(xq)),
inference(cnf_transformation,[],[f121]) ).
fof(f185,plain,
aVector0(xq),
inference(cnf_transformation,[],[f121]) ).
fof(f190,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[],[f46]) ).
fof(f192,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[],[f47]) ).
fof(f194,plain,
xE = sdtasasdt0(xp,xq),
inference(cnf_transformation,[],[f48]) ).
fof(f210,plain,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cnf_transformation,[],[f58]) ).
fof(f246,plain,
! [X0] :
( aNaturalNumber0(aDimensionOf0(X0))
| aVector0(X0) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f258,plain,
~ aVector0(xs),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f260,plain,
! [X0,X1] :
( aVector0(X1)
| aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1))) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f261,plain,
~ aVector0(xp),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f262,plain,
~ aVector0(xq),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f275,plain,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f276,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1)))
| aVector0(X1)
| aVector0(X0)
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xt)) ),
inference(forward_demodulation,[],[f260,f176]) ).
fof(f328,plain,
sz00 != aDimensionOf0(xt),
inference(superposition,[],[f177,f176]) ).
fof(f333,plain,
( aNaturalNumber0(aDimensionOf0(xt))
| aVector0(xs) ),
inference(superposition,[],[f246,f176]) ).
fof(f334,plain,
aNaturalNumber0(aDimensionOf0(xt)),
inference(forward_subsumption_resolution,[],[f333,f258]) ).
fof(f355,plain,
! [X0] :
( iLess0(aDimensionOf0(X0),szszuzczcdt0(aDimensionOf0(X0)))
| aVector0(X0) ),
inference(resolution,[],[f128,f246]) ).
fof(f637,plain,
( sz00 = aDimensionOf0(xt)
| aNaturalNumber0(sK0(aDimensionOf0(xt))) ),
inference(resolution,[],[f126,f334]) ).
fof(f638,plain,
aNaturalNumber0(sK0(aDimensionOf0(xt))),
inference(forward_subsumption_resolution,[],[f637,f328]) ).
fof(f914,plain,
( ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq)))
| aVector0(xq)
| aVector0(xp)
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(superposition,[],[f276,f194]) ).
fof(f929,plain,
( ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq)))
| aVector0(xp)
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(forward_subsumption_resolution,[],[f914,f262]) ).
fof(f940,definition,
( spl2_39
<=> iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f952,plain,
( ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq)))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(forward_subsumption_resolution,[],[f929,f261]) ).
fof(f958,plain,
( ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),xD))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(forward_demodulation,[],[f952,f192]) ).
fof(f959,plain,
( ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(forward_demodulation,[],[f958,f190]) ).
fof(f960,plain,
( aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
inference(forward_subsumption_resolution,[],[f959,f275]) ).
fof(f962,definition,
( spl2_43
<=> aDimensionOf0(xp) = aDimensionOf0(xq) ),
introduced(definition,[new_symbols(definition,[spl2_43])],[avatar_definition]) ).
fof(f964,plain,
( aDimensionOf0(xp) != aDimensionOf0(xq)
| spl2_43 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f965,plain,
( ~ spl2_39
| ~ spl2_43 ),
inference(avatar_split_clause,[],[f960,f962,f940]) ).
fof(f1131,plain,
( iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| aVector0(xp) ),
inference(superposition,[],[f355,f180]) ).
fof(f1134,plain,
iLess0(aDimensionOf0(xp),aDimensionOf0(xs)),
inference(forward_subsumption_resolution,[],[f1131,f261]) ).
fof(f1136,plain,
iLess0(aDimensionOf0(xp),aDimensionOf0(xt)),
inference(forward_demodulation,[],[f1134,f176]) ).
fof(f1137,plain,
spl2_39,
inference(avatar_split_clause,[],[f1136,f940]) ).
fof(f1217,plain,
( sz00 = aDimensionOf0(xt)
| aDimensionOf0(xt) = szszuzczcdt0(sK0(aDimensionOf0(xt))) ),
inference(resolution,[],[f125,f334]) ).
fof(f1304,plain,
aDimensionOf0(xt) = szszuzczcdt0(sK0(aDimensionOf0(xt))),
inference(forward_subsumption_resolution,[],[f1217,f328]) ).
fof(f1618,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| szszuzczcdt0(X0) != szszuzczcdt0(aDimensionOf0(X1))
| aDimensionOf0(X1) = X0
| aVector0(X1) ),
inference(resolution,[],[f127,f246]) ).
fof(f2895,plain,
! [X0] :
( szszuzczcdt0(aDimensionOf0(X0)) != szszuzczcdt0(sK0(aDimensionOf0(xt)))
| aDimensionOf0(X0) = sK0(aDimensionOf0(xt))
| aVector0(X0) ),
inference(resolution,[],[f1618,f638]) ).
fof(f2950,plain,
! [X0] :
( aDimensionOf0(xt) != szszuzczcdt0(aDimensionOf0(X0))
| aDimensionOf0(X0) = sK0(aDimensionOf0(xt))
| aVector0(X0) ),
inference(forward_demodulation,[],[f2895,f1304]) ).
fof(f10440,plain,
( aDimensionOf0(xs) != aDimensionOf0(xt)
| aDimensionOf0(xp) = sK0(aDimensionOf0(xt))
| aVector0(xp) ),
inference(superposition,[],[f2950,f180]) ).
fof(f10441,plain,
( aDimensionOf0(xt) != aDimensionOf0(xt)
| aDimensionOf0(xq) = sK0(aDimensionOf0(xt))
| aVector0(xq) ),
inference(superposition,[],[f2950,f184]) ).
fof(f10442,plain,
( aDimensionOf0(xq) = sK0(aDimensionOf0(xt))
| aVector0(xq) ),
inference(trivial_inequality_removal,[],[f10441]) ).
fof(f10443,plain,
aDimensionOf0(xq) = sK0(aDimensionOf0(xt)),
inference(forward_subsumption_resolution,[],[f10442,f262]) ).
fof(f10444,plain,
( aDimensionOf0(xp) = sK0(aDimensionOf0(xt))
| aVector0(xp) ),
inference(forward_subsumption_resolution,[],[f10440,f176]) ).
fof(f10446,plain,
aDimensionOf0(xp) = sK0(aDimensionOf0(xt)),
inference(forward_subsumption_resolution,[],[f10444,f261]) ).
fof(f13486,plain,
aDimensionOf0(xp) = aDimensionOf0(xq),
inference(superposition,[],[f10446,f10443]) ).
fof(f13571,plain,
( $false
| spl2_43 ),
inference(forward_subsumption_resolution,[],[f13486,f964]) ).
fof(f13572,plain,
spl2_43,
inference(avatar_contradiction_clause,[],[f13571]) ).
cnf(s41,plain,
( ~ spl2_39
| ~ spl2_43 ),
inference(sat_conversion,[],[f965]) ).
cnf(s46,plain,
spl2_39,
inference(sat_conversion,[],[f1137]) ).
cnf(s417,plain,
spl2_43,
inference(sat_conversion,[],[f13572]) ).
cnf(s430,plain,
$false,
inference(rat,[],[s41,s417,s46]) ).
fof(f13625,plain,
$false,
inference(avatar_sat_refutation,[],[s430]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG052+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.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 23:02:32 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 Running first-order model finding
% 0.15/0.41 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
% 5.49/1.28 % (282769)Will run a generic schedule for satisfiability detection.
% 5.49/1.28 % (282775)% WARNING: option uhcvi not known.
% 5.49/1.28 % (282775)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3497078247:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.49/1.28 % (282774)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2092524205_2999 on theBenchmark for (2999ds/0Mi)
% 5.49/1.28 % (282776)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1909925726:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.49/1.28 % (282780)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=145099698:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.49/1.28 % (282777)dis+10_1_sil=32000:sp=arity:random_seed=4288708842:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.49/1.28 % (282779)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1648020490:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.49/1.28 % (282778)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2498990966:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.49/1.28 % TRYING [1]
% 5.49/1.28 % TRYING [2]
% 5.49/1.28 % TRYING [3]
% 5.49/1.28 % TRYING [4]
% 5.49/1.28 % (282777)Instruction limit reached!
% 5.49/1.28 % (282777)------------------------------
% 5.49/1.28 % (282777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282777)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282777)Termination reason: Instruction limit
% 5.49/1.28 % (282777)Termination phase: Saturation
% 5.49/1.28 % (282777)Time elapsed: 0.061 s
% 5.49/1.28 % (282777)Peak memory usage: 12 MB
% 5.49/1.28 % (282777)Instructions burned: 103 (million)
% 5.49/1.28 % (282778)Instruction limit reached!
% 5.49/1.28 % (282778)------------------------------
% 5.49/1.28 % (282778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282778)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282778)Termination reason: Instruction limit
% 5.49/1.28 % (282778)Termination phase: Saturation
% 5.49/1.28 % (282778)Time elapsed: 0.066 s
% 5.49/1.28 % (282778)Peak memory usage: 13 MB
% 5.49/1.28 % (282778)Instructions burned: 116 (million)
% 5.49/1.28 % (282779)Instruction limit reached!
% 5.49/1.28 % (282779)------------------------------
% 5.49/1.28 % (282779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282779)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282779)Termination reason: Instruction limit
% 5.49/1.28 % (282779)Termination phase: Saturation
% 5.49/1.28 % (282779)Time elapsed: 0.070 s
% 5.49/1.28 % (282779)Peak memory usage: 13 MB
% 5.49/1.28 % (282779)Instructions burned: 132 (million)
% 5.49/1.28 % TRYING [5]
% 5.49/1.28 % (282788)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=569220293:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.49/1.28 % (282789)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1403491882:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.49/1.28 % (282790)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2743379305:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.49/1.28 % TRYING [1]
% 5.49/1.28 % TRYING [2]
% 5.49/1.28 % (282780)Instruction limit reached!
% 5.49/1.28 % (282780)------------------------------
% 5.49/1.28 % (282780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282780)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282780)Termination reason: Instruction limit
% 5.49/1.28 % (282780)Termination phase: Saturation
% 5.49/1.28 % (282780)Time elapsed: 0.092 s
% 5.49/1.28 % (282780)Peak memory usage: 14 MB
% 5.49/1.28 % (282780)Instructions burned: 160 (million)
% 5.49/1.28 % TRYING [3]
% 5.49/1.28 % TRYING [4]
% 5.49/1.28 % (282794)ott-21_1_sil=16000:fs=off:random_seed=4064911244:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.49/1.28 % (282789)Instruction limit reached!
% 5.49/1.28 % (282789)------------------------------
% 5.49/1.28 % (282789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282789)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282789)Termination reason: Instruction limit
% 5.49/1.28 % (282789)Termination phase: Saturation
% 5.49/1.28 % (282789)Time elapsed: 0.060 s
% 5.49/1.28 % (282789)Peak memory usage: 12 MB
% 5.49/1.28 % (282789)Instructions burned: 133 (million)
% 5.49/1.28 % TRYING [5]
% 5.49/1.28 % (282796)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=663308461:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.49/1.28 % (282794)Instruction limit reached!
% 5.49/1.28 % (282794)------------------------------
% 5.49/1.28 % (282794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282794)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282794)Termination reason: Instruction limit
% 5.49/1.28 % (282794)Termination phase: Saturation
% 5.49/1.28 % (282794)Time elapsed: 0.089 s
% 5.49/1.28 % (282794)Peak memory usage: 13 MB
% 5.49/1.28 % (282794)Instructions burned: 180 (million)
% 5.49/1.28 % (282798)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2957015535:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.49/1.28 % TRYING [1]
% 5.49/1.28 % TRYING [2]
% 5.49/1.28 % TRYING [6]
% 5.49/1.28 % TRYING [3]
% 5.49/1.28 % TRYING [4]
% 5.49/1.28 % TRYING [6]
% 5.49/1.28 % (282788)Instruction limit reached!
% 5.49/1.28 % (282788)------------------------------
% 5.49/1.28 % (282788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282788)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282788)Termination reason: Instruction limit
% 5.49/1.28 % (282788)Termination phase: Finite model building constraint generation
% 5.49/1.28 % (282788)Time elapsed: 0.258 s
% 5.49/1.28 % (282788)Peak memory usage: 36 MB
% 5.49/1.28 % (282788)Instructions burned: 716 (million)
% 5.49/1.28 % (282800)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1747072403:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 5.49/1.28 % (282790)Instruction limit reached!
% 5.49/1.28 % (282790)------------------------------
% 5.49/1.28 % (282790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282790)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282790)Termination reason: Instruction limit
% 5.49/1.28 % (282790)Termination phase: Saturation
% 5.49/1.28 % (282790)Time elapsed: 0.321 s
% 5.49/1.28 % (282790)Peak memory usage: 19 MB
% 5.49/1.28 % (282790)Instructions burned: 684 (million)
% 5.49/1.28 % (282802)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3817410849:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.49/1.28 % (282796)Instruction limit reached!
% 5.49/1.28 % (282796)------------------------------
% 5.49/1.28 % (282796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282796)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282796)Termination reason: Instruction limit
% 5.49/1.28 % (282796)Termination phase: Saturation
% 5.49/1.28 % (282796)Time elapsed: 0.299 s
% 5.49/1.28 % (282796)Peak memory usage: 14 MB
% 5.49/1.28 % (282796)Instructions burned: 478 (million)
% 5.49/1.28 % (282804)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3241883065:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 5.49/1.28 % TRYING [5]
% 5.49/1.28 % (282798)Instruction limit reached!
% 5.49/1.28 % (282798)------------------------------
% 5.49/1.28 % (282798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.28 % (282798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.28 % (282798)CaDiCaL version: 2.1.3
% 5.49/1.28 % (282798)Termination reason: Instruction limit
% 5.49/1.28 % (282798)Termination phase: Finite model building constraint generation
% 5.49/1.28 % (282798)Time elapsed: 0.322 s
% 5.49/1.28 % (282798)Peak memory usage: 20 MB
% 5.49/1.28 % (282798)Instructions burned: 867 (million)
% 5.49/1.28 % (282806)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2044890984:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.49/1.28 % TRYING [7]
% 5.49/1.28 % (282804) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-282769-282804"...
% 5.49/1.28 % (282804)...printing done.
% 5.49/1.28 % (282804)Refutation found. Thanks to Tanya!
% 5.49/1.28 % SZS status Theorem for theBenchmark
% 5.49/1.28 % SZS output start Proof for theBenchmark
% See solution above
% 5.49/1.29 % (282804)------------------------------
% 5.49/1.29 % (282804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.49/1.29 % (282804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.49/1.29 % (282804)CaDiCaL version: 2.1.3
% 5.49/1.29 % (282804)Termination reason: Refutation
% 5.49/1.29 % (282804)Time elapsed: 0.324 s
% 5.49/1.29 % (282804)Peak memory usage: 18 MB
% 5.49/1.29 % (282804)Instructions burned: 599 (million)
% 5.49/1.29 % (282769)Success in time 0.87 s
% 5.49/1.29 % Vampire exiting
%------------------------------------------------------------------------------