%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG080+1 : 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 : n002.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 24.29s 4.03s
% Output : Refutation 24.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 21
% Syntax : Number of formulae : 84 ( 58 unt; 5 def)
% Number of atoms : 134 ( 86 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 85 ( 35 ~; 35 |; 13 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-2 aty)
% Number of variables : 15 ( 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f36,axiom,
! [X0,X1] :
( ( aVector0(X0)
& aVector0(X1) )
=> ( ( aDimensionOf0(X0) = aDimensionOf0(X1)
& aDimensionOf0(X1) != sz00 )
=> sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSPN) ).
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,axiom,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1692) ).
fof(f42,axiom,
( aVector0(xp)
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1709) ).
fof(f43,axiom,
( aVector0(xq)
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1726) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1746) ).
fof(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1766) ).
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(f49,axiom,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1837) ).
fof(f50,axiom,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1854) ).
fof(f51,axiom,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1873) ).
fof(f58,axiom,
sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2733) ).
fof(f59,conjecture,
sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f60,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f66,plain,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(flattening,[],[f60]) ).
fof(f116,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(ennf_transformation,[],[f36]) ).
fof(f117,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(flattening,[],[f116]) ).
fof(f175,plain,
! [X0,X1] :
( aDimensionOf0(X0) != aDimensionOf0(X1)
| sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| sz00 = aDimensionOf0(X1)
| ~ aVector0(X0)
| ~ aVector0(X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f177,plain,
aVector0(xt),
inference(cnf_transformation,[],[f38]) ).
fof(f178,plain,
aVector0(xs),
inference(cnf_transformation,[],[f38]) ).
fof(f180,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[],[f40]) ).
fof(f181,plain,
sz00 != aDimensionOf0(xs),
inference(cnf_transformation,[],[f41]) ).
fof(f182,plain,
xp = sziznziztdt0(xs),
inference(cnf_transformation,[],[f42]) ).
fof(f184,plain,
xq = sziznziztdt0(xt),
inference(cnf_transformation,[],[f43]) ).
fof(f186,plain,
xA = sdtlbdtrb0(xs,aDimensionOf0(xs)),
inference(cnf_transformation,[],[f44]) ).
fof(f188,plain,
xB = sdtlbdtrb0(xt,aDimensionOf0(xt)),
inference(cnf_transformation,[],[f45]) ).
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(f196,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[],[f49]) ).
fof(f198,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[],[f50]) ).
fof(f200,plain,
xH = sdtasdt0(xA,xB),
inference(cnf_transformation,[],[f51]) ).
fof(f212,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(cnf_transformation,[],[f58]) ).
fof(f213,plain,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(cnf_transformation,[],[f66]) ).
fof(f217,definition,
sF2 = sdtasasdt0(xs,xt),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f218,plain,
sdtasasdt0(xs,xt) = sF2,
inference(reorient_equations,[],[f217]) ).
fof(f219,definition,
sF3 = sdtasdt0(sF2,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f220,plain,
sdtasdt0(sF2,sF2) = sF3,
inference(reorient_equations,[],[f219]) ).
fof(f221,definition,
sF4 = sdtasasdt0(xs,xs),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f222,plain,
sdtasasdt0(xs,xs) = sF4,
inference(reorient_equations,[],[f221]) ).
fof(f223,definition,
sF5 = sdtasasdt0(xt,xt),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f224,plain,
sdtasasdt0(xt,xt) = sF5,
inference(reorient_equations,[],[f223]) ).
fof(f225,definition,
sF6 = sdtasdt0(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f226,plain,
sdtasdt0(sF4,sF5) = sF6,
inference(reorient_equations,[],[f225]) ).
fof(f227,plain,
~ sdtlseqdt0(sF3,sF6),
inference(definition_folding,[],[f213,f226,f224,f222,f220,f218,f218]) ).
fof(f230,plain,
xB = sdtlbdtrb0(xt,aDimensionOf0(xs)),
inference(superposition,[],[f188,f180]) ).
fof(f1020,plain,
! [X0] :
( aDimensionOf0(X0) != aDimensionOf0(xs)
| sdtasasdt0(X0,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xt,aDimensionOf0(xs))))
| sz00 = aDimensionOf0(xs)
| ~ aVector0(X0)
| ~ aVector0(xt) ),
inference(superposition,[],[f175,f180]) ).
fof(f1021,plain,
! [X0] :
( sdtasasdt0(X0,X0) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X0)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X0,aDimensionOf0(X0))))
| sz00 = aDimensionOf0(X0)
| ~ aVector0(X0)
| ~ aVector0(X0) ),
inference(equality_resolution,[],[f175]) ).
fof(f1022,plain,
! [X0] :
( ~ aVector0(X0)
| sz00 = aDimensionOf0(X0)
| sdtasasdt0(X0,X0) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X0)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X0,aDimensionOf0(X0)))) ),
inference(duplicate_literal_removal,[],[f1021]) ).
fof(f1023,plain,
! [X0] :
( aDimensionOf0(X0) != aDimensionOf0(xs)
| sdtasasdt0(X0,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xt,aDimensionOf0(xs))))
| ~ aVector0(X0)
| ~ aVector0(xt) ),
inference(forward_subsumption_resolution,[],[f1020,f181]) ).
fof(f1025,plain,
! [X0] :
( aDimensionOf0(X0) != aDimensionOf0(xs)
| sdtasasdt0(X0,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xt,aDimensionOf0(xs))))
| ~ aVector0(X0) ),
inference(forward_subsumption_resolution,[],[f1023,f177]) ).
fof(f1027,plain,
! [X0] :
( sdtasasdt0(X0,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xt)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ),
inference(forward_demodulation,[],[f1025,f230]) ).
fof(f1029,plain,
! [X0] :
( aDimensionOf0(X0) != aDimensionOf0(xs)
| sdtasasdt0(X0,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),xq),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),xB))
| ~ aVector0(X0) ),
inference(forward_demodulation,[],[f1027,f184]) ).
fof(f13211,plain,
( aDimensionOf0(xs) != aDimensionOf0(xs)
| sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xs)),xB))
| ~ aVector0(xt) ),
inference(superposition,[],[f1029,f180]) ).
fof(f13213,plain,
( sdtasasdt0(xs,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB))
| ~ aVector0(xs) ),
inference(equality_resolution,[],[f1029]) ).
fof(f13214,plain,
( sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xs)),xB))
| ~ aVector0(xt) ),
inference(trivial_inequality_removal,[],[f13211]) ).
fof(f13215,plain,
sdtasasdt0(xs,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),xB)),
inference(forward_subsumption_resolution,[],[f13213,f178]) ).
fof(f13217,plain,
sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(sdtlbdtrb0(xt,aDimensionOf0(xs)),xB)),
inference(forward_subsumption_resolution,[],[f13214,f177]) ).
fof(f13218,plain,
sdtasasdt0(xs,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),sdtasdt0(xA,xB)),
inference(forward_demodulation,[],[f13215,f186]) ).
fof(f13220,plain,
sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),sdtasdt0(xB,xB)),
inference(forward_demodulation,[],[f13217,f230]) ).
fof(f13221,plain,
sdtasasdt0(xs,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),xq),xH),
inference(forward_demodulation,[],[f13218,f200]) ).
fof(f13222,plain,
sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(sziznziztdt0(xt),xq),xG),
inference(forward_demodulation,[],[f13220,f198]) ).
fof(f13223,plain,
sdtasasdt0(xs,xt) = sdtpldt0(sdtasasdt0(xp,xq),xH),
inference(forward_demodulation,[],[f13221,f182]) ).
fof(f13224,plain,
sdtasasdt0(xt,xt) = sdtpldt0(sdtasasdt0(xq,xq),xG),
inference(forward_demodulation,[],[f13222,f184]) ).
fof(f13225,plain,
sdtpldt0(xE,xH) = sdtasasdt0(xs,xt),
inference(forward_demodulation,[],[f13223,f194]) ).
fof(f13226,plain,
sdtpldt0(xD,xG) = sdtasasdt0(xt,xt),
inference(forward_demodulation,[],[f13224,f192]) ).
fof(f13227,plain,
sdtpldt0(xE,xH) = sF2,
inference(forward_demodulation,[],[f13225,f218]) ).
fof(f13228,plain,
sdtpldt0(xD,xG) = sF5,
inference(forward_demodulation,[],[f13226,f224]) ).
fof(f13229,plain,
sdtlseqdt0(sdtasdt0(sF2,sF2),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(superposition,[],[f212,f13227]) ).
fof(f13241,plain,
sdtlseqdt0(sdtasdt0(sF2,sF2),sdtasdt0(sdtpldt0(xC,xF),sF5)),
inference(forward_demodulation,[],[f13229,f13228]) ).
fof(f13247,plain,
sdtlseqdt0(sF3,sdtasdt0(sdtpldt0(xC,xF),sF5)),
inference(forward_demodulation,[],[f13241,f220]) ).
fof(f13910,plain,
( sz00 = aDimensionOf0(xs)
| sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(resolution,[],[f1022,f178]) ).
fof(f13917,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(forward_subsumption_resolution,[],[f13910,f181]) ).
fof(f13921,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(xA,xA)),
inference(forward_demodulation,[],[f13917,f186]) ).
fof(f13924,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xF),
inference(forward_demodulation,[],[f13921,f196]) ).
fof(f13927,plain,
sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(xp,xp),xF),
inference(forward_demodulation,[],[f13924,f182]) ).
fof(f13929,plain,
sdtpldt0(xC,xF) = sdtasasdt0(xs,xs),
inference(forward_demodulation,[],[f13927,f190]) ).
fof(f13931,plain,
sdtpldt0(xC,xF) = sF4,
inference(forward_demodulation,[],[f13929,f222]) ).
fof(f13933,plain,
sdtlseqdt0(sF3,sdtasdt0(sF4,sF5)),
inference(superposition,[],[f13247,f13931]) ).
fof(f13945,plain,
sdtlseqdt0(sF3,sF6),
inference(forward_demodulation,[],[f13933,f226]) ).
fof(f13950,plain,
$false,
inference(forward_subsumption_resolution,[],[f13945,f227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG080+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 23:11:37 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 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
% 13.19/2.37 % (3998540)Will run a generic schedule for satisfiability detection.
% 13.19/2.37 % (3998548)dis+10_1_sil=32000:sp=arity:random_seed=3482847219:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.19/2.37 % (3998546)% WARNING: option uhcvi not known.
% 13.19/2.37 % (3998545)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2355203269_2999 on theBenchmark for (2999ds/0Mi)
% 13.19/2.37 % (3998546)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4099990431:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.19/2.37 % (3998547)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1904211431:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.19/2.37 % (3998549)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3515243131:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.19/2.37 % (3998551)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2253744080:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.19/2.37 % (3998550)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2998297139:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.19/2.37 % TRYING [1]
% 13.19/2.37 % TRYING [2]
% 13.19/2.37 % TRYING [3]
% 13.19/2.37 % TRYING [4]
% 13.19/2.37 % (3998548)Instruction limit reached!
% 13.19/2.37 % (3998548)------------------------------
% 13.19/2.37 % (3998548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.19/2.37 % (3998548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.37 % (3998548)CaDiCaL version: 2.1.3
% 13.19/2.37 % (3998548)Termination reason: Instruction limit
% 13.19/2.37 % (3998548)Termination phase: Saturation
% 13.19/2.37 % (3998548)Time elapsed: 0.036 s
% 13.19/2.37 % (3998548)Peak memory usage: 13 MB
% 13.19/2.37 % (3998548)Instructions burned: 106 (million)
% 13.19/2.37 % (3998559)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=691827147:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.19/2.37 % TRYING [1]
% 13.19/2.37 % TRYING [2]
% 13.19/2.37 % TRYING [3]
% 13.19/2.37 % TRYING [4]
% 13.19/2.37 % (3998549)Instruction limit reached!
% 13.19/2.37 % (3998549)------------------------------
% 13.19/2.37 % (3998549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.19/2.37 % (3998549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.37 % (3998549)CaDiCaL version: 2.1.3
% 13.19/2.37 % (3998549)Termination reason: Instruction limit
% 13.19/2.37 % (3998549)Termination phase: Saturation
% 13.19/2.37 % (3998549)Time elapsed: 0.067 s
% 13.19/2.37 % (3998549)Peak memory usage: 13 MB
% 13.19/2.37 % (3998549)Instructions burned: 116 (million)
% 13.19/2.37 % (3998550)Instruction limit reached!
% 13.19/2.37 % (3998550)------------------------------
% 13.19/2.37 % (3998550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.19/2.37 % (3998550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.37 % (3998550)CaDiCaL version: 2.1.3
% 13.19/2.37 % (3998550)Termination reason: Instruction limit
% 13.19/2.37 % (3998550)Termination phase: Saturation
% 13.19/2.37 % (3998550)Time elapsed: 0.072 s
% 13.19/2.37 % (3998550)Peak memory usage: 13 MB
% 13.19/2.37 % (3998550)Instructions burned: 131 (million)
% 13.19/2.37 % TRYING [5]
% 13.19/2.37 % TRYING [5]
% 13.19/2.37 % (3998561)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3487664658:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.19/2.37 % (3998562)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=2582389840:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.19/2.37 % (3998551)Instruction limit reached!
% 13.19/2.37 % (3998551)------------------------------
% 13.19/2.37 % (3998551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.19/2.37 % (3998551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.19/2.37 % (3998551)CaDiCaL version: 2.1.3
% 13.19/2.37 % (3998551)Termination reason: Instruction limit
% 13.19/2.37 % (3998551)Termination phase: Saturation
% 13.19/2.37 % (3998551)Time elapsed: 0.100 s
% 13.19/2.37 % (3998551)Peak memory usage: 14 MB
% 13.19/2.37 % (3998551)Instructions burned: 160 (million)
% 13.19/2.37 % (3998565)ott-21_1_sil=16000:fs=off:random_seed=253359558:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.19/2.37 % (3998561)Instruction limit reached!
% 13.19/2.37 % (3998561)------------------------------
% 13.19/2.37 % (3998561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998561)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998561)Termination reason: Instruction limit
% 24.29/4.03 % (3998561)Termination phase: Saturation
% 24.29/4.03 % (3998561)Time elapsed: 0.061 s
% 24.29/4.03 % (3998561)Peak memory usage: 12 MB
% 24.29/4.03 % (3998561)Instructions burned: 133 (million)
% 24.29/4.03 % (3998567)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=467997000:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.29/4.03 % TRYING [6]
% 24.29/4.03 % (3998559)Instruction limit reached!
% 24.29/4.03 % (3998559)------------------------------
% 24.29/4.03 % (3998559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998559)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998559)Termination reason: Instruction limit
% 24.29/4.03 % (3998559)Termination phase: Finite model building constraint generation
% 24.29/4.03 % (3998559)Time elapsed: 0.144 s
% 24.29/4.03 % (3998559)Peak memory usage: 38 MB
% 24.29/4.03 % (3998559)Instructions burned: 718 (million)
% 24.29/4.03 % (3998569)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=676531420:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 24.29/4.03 % TRYING [1]
% 24.29/4.03 % TRYING [2]
% 24.29/4.03 % TRYING [3]
% 24.29/4.03 % (3998565)Instruction limit reached!
% 24.29/4.03 % (3998565)------------------------------
% 24.29/4.03 % (3998565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998565)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998565)Termination reason: Instruction limit
% 24.29/4.03 % (3998565)Termination phase: Saturation
% 24.29/4.03 % (3998565)Time elapsed: 0.091 s
% 24.29/4.03 % (3998565)Peak memory usage: 13 MB
% 24.29/4.03 % (3998565)Instructions burned: 181 (million)
% 24.29/4.03 % (3998571)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=91153708:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 24.29/4.03 % TRYING [6]
% 24.29/4.03 % TRYING [4]
% 24.29/4.03 % TRYING [5]
% 24.29/4.03 % (3998569)Instruction limit reached!
% 24.29/4.03 % (3998569)------------------------------
% 24.29/4.03 % (3998569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998569)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998569)Termination reason: Instruction limit
% 24.29/4.03 % (3998569)Termination phase: Finite model building constraint generation
% 24.29/4.03 % (3998569)Time elapsed: 0.172 s
% 24.29/4.03 % (3998569)Peak memory usage: 20 MB
% 24.29/4.03 % (3998569)Instructions burned: 869 (million)
% 24.29/4.03 % (3998573)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=261921573:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 24.29/4.03 % (3998562)Instruction limit reached!
% 24.29/4.03 % (3998562)------------------------------
% 24.29/4.03 % (3998562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998562)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998562)Termination reason: Instruction limit
% 24.29/4.03 % (3998562)Termination phase: Saturation
% 24.29/4.03 % (3998562)Time elapsed: 0.301 s
% 24.29/4.03 % (3998562)Peak memory usage: 16 MB
% 24.29/4.03 % (3998562)Instructions burned: 684 (million)
% 24.29/4.03 % (3998575)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=3014491583:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 24.29/4.03 % (3998567)Instruction limit reached!
% 24.29/4.03 % (3998567)------------------------------
% 24.29/4.03 % (3998567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998567)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998567)Termination reason: Instruction limit
% 24.29/4.03 % (3998567)Termination phase: Saturation
% 24.29/4.03 % (3998567)Time elapsed: 0.300 s
% 24.29/4.03 % (3998567)Peak memory usage: 15 MB
% 24.29/4.03 % (3998567)Instructions burned: 478 (million)
% 24.29/4.03 % (3998577)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=76586856:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 24.29/4.03 % (3998573)Instruction limit reached!
% 24.29/4.03 % (3998573)------------------------------
% 24.29/4.03 % (3998573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998573)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998573)Termination reason: Instruction limit
% 24.29/4.03 % (3998573)Termination phase: Finite model building constraint generation
% 24.29/4.03 % (3998573)Time elapsed: 0.238 s
% 24.29/4.03 % (3998573)Peak memory usage: 104 MB
% 24.29/4.03 % (3998573)Instructions burned: 893 (million)
% 24.29/4.03 % TRYING [7]
% 24.29/4.03 % (3998579)fmb+10_1_sil=64000:random_seed=1044122523:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 24.29/4.03 % TRYING [1]
% 24.29/4.03 % TRYING [2]
% 24.29/4.03 % TRYING [3]
% 24.29/4.03 % TRYING [4]
% 24.29/4.03 % (3998575)Instruction limit reached!
% 24.29/4.03 % (3998575)------------------------------
% 24.29/4.03 % (3998575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998575)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998575)Termination reason: Instruction limit
% 24.29/4.03 % (3998575)Termination phase: Saturation
% 24.29/4.03 % (3998575)Time elapsed: 0.382 s
% 24.29/4.03 % (3998575)Peak memory usage: 22 MB
% 24.29/4.03 % (3998575)Instructions burned: 692 (million)
% 24.29/4.03 % TRYING [5]
% 24.29/4.03 % (3998581)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3691554216:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 24.29/4.03 % TRYING [20]
% 24.29/4.03 % (3998571)Instruction limit reached!
% 24.29/4.03 % (3998571)------------------------------
% 24.29/4.03 % (3998571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998571)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998571)Termination reason: Instruction limit
% 24.29/4.03 % (3998571)Termination phase: Saturation
% 24.29/4.03 % (3998571)Time elapsed: 0.620 s
% 24.29/4.03 % (3998571)Peak memory usage: 27 MB
% 24.29/4.03 % (3998571)Instructions burned: 1180 (million)
% 24.29/4.03 % (3998583)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2549657199:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 24.29/4.03 % TRYING [8]
% 24.29/4.03 % (3998577)Instruction limit reached!
% 24.29/4.03 % (3998577)------------------------------
% 24.29/4.03 % (3998577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998577)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998577)Termination reason: Instruction limit
% 24.29/4.03 % (3998577)Termination phase: Saturation
% 24.29/4.03 % (3998577)Time elapsed: 0.495 s
% 24.29/4.03 % (3998577)Peak memory usage: 21 MB
% 24.29/4.03 % (3998577)Instructions burned: 881 (million)
% 24.29/4.03 % (3998585)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1879390027:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 24.29/4.03 % (3998583)Instruction limit reached!
% 24.29/4.03 % (3998583)------------------------------
% 24.29/4.03 % (3998583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998583)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998583)Termination reason: Instruction limit
% 24.29/4.03 % (3998583)Termination phase: Finite model building constraint generation
% 24.29/4.03 % (3998583)Time elapsed: 0.306 s
% 24.29/4.03 % (3998583)Peak memory usage: 63 MB
% 24.29/4.03 % (3998583)Instructions burned: 920 (million)
% 24.29/4.03 % (3998587)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=329616234:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 24.29/4.03 % TRYING [6]
% 24.29/4.03 % TRYING [8]
% 24.29/4.03 % (3998587)Instruction limit reached!
% 24.29/4.03 % (3998587)------------------------------
% 24.29/4.03 % (3998587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998587)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998587)Termination reason: Instruction limit
% 24.29/4.03 % (3998587)Termination phase: Saturation
% 24.29/4.03 % (3998587)Time elapsed: 0.679 s
% 24.29/4.03 % (3998587)Peak memory usage: 19 MB
% 24.29/4.03 % (3998587)Instructions burned: 1472 (million)
% 24.29/4.03 % (3998589)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=469185474:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 24.29/4.03 % (3998589)Cannot represent all propositional literals internally
% 24.29/4.03 % (3998589)Refutation not found, incomplete strategy
% 24.29/4.03 % (3998589)------------------------------
% 24.29/4.03 % (3998589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998589)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998589)Termination reason: Refutation not found, incomplete strategy
% 24.29/4.03 % (3998589)Time elapsed: 0.008 s
% 24.29/4.03 % (3998589)Peak memory usage: 11 MB
% 24.29/4.03 % (3998589)Instructions burned: 15 (million)
% 24.29/4.03 % (3998589)------------------------------
% 24.29/4.03 % (3998589)------------------------------
% 24.29/4.03 % (3998591)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4290145654:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 24.29/4.03 % TRYING [16]
% 24.29/4.03 % TRYING [7]
% 24.29/4.03 % (3998591)Instruction limit reached!
% 24.29/4.03 % (3998591)------------------------------
% 24.29/4.03 % (3998591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998591)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998591)Termination reason: Instruction limit
% 24.29/4.03 % (3998591)Termination phase: Finite model building constraint generation
% 24.29/4.03 % (3998591)Time elapsed: 0.761 s
% 24.29/4.03 % (3998591)Peak memory usage: 146 MB
% 24.29/4.03 % (3998591)Instructions burned: 2177 (million)
% 24.29/4.03 % (3998593)ott-2_1_sil=16000:newcnf=on:random_seed=2985824197:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 24.29/4.03 % (3998593)Instruction limit reached!
% 24.29/4.03 % (3998593)------------------------------
% 24.29/4.03 % (3998593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998593)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998593)Termination reason: Instruction limit
% 24.29/4.03 % (3998593)Termination phase: Saturation
% 24.29/4.03 % (3998593)Time elapsed: 0.437 s
% 24.29/4.03 % (3998593)Peak memory usage: 24 MB
% 24.29/4.03 % (3998593)Instructions burned: 870 (million)
% 24.29/4.03 % (3998595)ott+10_1_sil=32000:tgt=ground:random_seed=802376891:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 24.29/4.03 % (3998595) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3998540-3998595"...
% 24.29/4.03 % (3998595)...printing done.
% 24.29/4.03 % (3998595)Refutation found. Thanks to Tanya!
% 24.29/4.03 % SZS status Theorem for theBenchmark
% 24.29/4.03 % SZS output start Proof for theBenchmark
% See solution above
% 24.29/4.03 % (3998595)------------------------------
% 24.29/4.03 % (3998595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.29/4.03 % (3998595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/4.03 % (3998595)CaDiCaL version: 2.1.3
% 24.29/4.03 % (3998595)Termination reason: Refutation
% 24.29/4.03 % (3998595)Time elapsed: 0.297 s
% 24.29/4.03 % (3998595)Peak memory usage: 20 MB
% 24.29/4.03 % (3998595)Instructions burned: 563 (million)
% 24.29/4.03 % (3998540)Success in time 3.601 s
% 24.29/4.03 % Vampire exiting
%------------------------------------------------------------------------------