%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG073+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 : Tue Sep 29 12:35:56 PM UTC 2026
% Result : Theorem 15.12s 7.67s
% Output : Refutation 15.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of formulae : 83 ( 22 unt; 5 def)
% Number of atoms : 217 ( 32 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 248 ( 114 ~; 112 |; 11 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 35 ( 0 sgn 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f21,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
fof(f28,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(sz0z00,X0)
& sdtlseqdt0(sz0z00,X1)
& sdtasdt0(X0,X0) = sdtasdt0(X1,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqrt) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
fof(f53,axiom,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
fof(f54,axiom,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
fof(f59,axiom,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2405) ).
fof(f62,axiom,
( sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
& sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2628) ).
fof(f63,axiom,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2654) ).
fof(f64,conjecture,
sdtpldt0(xR,xS) = sdtpldt0(xP,xP),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f65,negated_conjecture,
sdtpldt0(xR,xS) != sdtpldt0(xP,xP),
inference(negated_conjecture,[status(cth)],[f64]) ).
fof(f66,plain,
sdtpldt0(xP,xP) != sdtpldt0(xR,xS),
inference(flattening,[],[f65]) ).
fof(f77,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f78,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f80,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f79]) ).
fof(f96,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f97,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f96]) ).
fof(f109,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f110,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f109]) ).
fof(f136,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f137,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f80]) ).
fof(f158,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f97]) ).
fof(f166,plain,
! [X0,X1] :
( sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f205,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f207,plain,
aScalar0(xP),
inference(cnf_transformation,[],[f53]) ).
fof(f209,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f215,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(cnf_transformation,[],[f59]) ).
fof(f218,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)),
inference(cnf_transformation,[],[f62]) ).
fof(f219,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(cnf_transformation,[],[f62]) ).
fof(f220,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
inference(cnf_transformation,[],[f63]) ).
fof(f221,plain,
sdtpldt0(xP,xP) != sdtpldt0(xR,xS),
inference(cnf_transformation,[],[f66]) ).
fof(f658,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) ),
inference(resolution,[],[f220,f158]) ).
fof(f659,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) ),
inference(forward_subsumption_resolution,[],[f658,f215]) ).
fof(f26484,definition,
( spl2_33
<=> aScalar0(sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f26485,plain,
( aScalar0(sdtpldt0(xR,xS))
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f26484]) ).
fof(f26486,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| spl2_33 ),
inference(avatar_component_clause,[],[f26484]) ).
fof(f26488,definition,
( spl2_34
<=> aScalar0(sdtpldt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
fof(f26489,plain,
( aScalar0(sdtpldt0(xP,xP))
| ~ spl2_34 ),
inference(avatar_component_clause,[],[f26488]) ).
fof(f26490,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| spl2_34 ),
inference(avatar_component_clause,[],[f26488]) ).
fof(f26495,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| spl2_33 ),
inference(resolution,[],[f26486,f136]) ).
fof(f26496,plain,
( ~ aScalar0(xS)
| spl2_33 ),
inference(forward_subsumption_resolution,[],[f26495,f205]) ).
fof(f26497,plain,
( $false
| spl2_33 ),
inference(forward_subsumption_resolution,[],[f26496,f209]) ).
fof(f26498,plain,
spl2_33,
inference(avatar_contradiction_clause,[],[f26497]) ).
fof(f27067,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| spl2_34 ),
inference(resolution,[],[f26490,f136]) ).
fof(f27068,plain,
( ~ aScalar0(xP)
| spl2_34 ),
inference(duplicate_literal_removal,[],[f27067]) ).
fof(f27069,plain,
( $false
| spl2_34 ),
inference(forward_subsumption_resolution,[],[f27068,f207]) ).
fof(f27070,plain,
spl2_34,
inference(avatar_contradiction_clause,[],[f27069]) ).
fof(f46111,definition,
( spl2_54
<=> sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_54])],[avatar_definition]) ).
fof(f46113,plain,
( sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) = sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))
| ~ spl2_54 ),
inference(avatar_component_clause,[],[f46111]) ).
fof(f46115,definition,
( spl2_55
<=> aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f46117,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| spl2_55 ),
inference(avatar_component_clause,[],[f46115]) ).
fof(f46119,definition,
( spl2_56
<=> aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))) ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f46121,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)))
| spl2_56 ),
inference(avatar_component_clause,[],[f46119]) ).
fof(f46122,plain,
( spl2_54
| ~ spl2_55
| ~ spl2_56 ),
inference(avatar_split_clause,[],[f659,f46119,f46115,f46111]) ).
fof(f46156,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| ~ aScalar0(sdtpldt0(xR,xS))
| spl2_55 ),
inference(resolution,[],[f46117,f137]) ).
fof(f46157,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| spl2_55 ),
inference(duplicate_literal_removal,[],[f46156]) ).
fof(f46158,plain,
( $false
| ~ spl2_33
| spl2_55 ),
inference(forward_subsumption_resolution,[],[f46157,f26485]) ).
fof(f46159,plain,
( ~ spl2_33
| spl2_55 ),
inference(avatar_contradiction_clause,[],[f46158]) ).
fof(f47117,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| ~ aScalar0(sdtpldt0(xP,xP))
| spl2_56 ),
inference(resolution,[],[f46121,f137]) ).
fof(f47118,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| spl2_56 ),
inference(duplicate_literal_removal,[],[f47117]) ).
fof(f47119,plain,
( $false
| ~ spl2_34
| spl2_56 ),
inference(forward_subsumption_resolution,[],[f47118,f26489]) ).
fof(f47120,plain,
( ~ spl2_34
| spl2_56 ),
inference(avatar_contradiction_clause,[],[f47119]) ).
fof(f48082,plain,
( ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))
| ~ aScalar0(sdtpldt0(xR,xS))
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
| sdtpldt0(xR,xS) = X0 )
| ~ spl2_54 ),
inference(superposition,[],[f166,f46113]) ).
fof(f48124,plain,
( ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
| sdtpldt0(xR,xS) = X0 )
| ~ spl2_33
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f48082,f26485]) ).
fof(f48135,plain,
( ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,X0)
| sdtpldt0(xR,xS) = X0 )
| ~ spl2_33
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f48124,f219]) ).
fof(f53658,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| sdtpldt0(xP,xP) = sdtpldt0(xR,xS)
| ~ spl2_33
| ~ spl2_54 ),
inference(equality_resolution,[],[f48135]) ).
fof(f53659,plain,
( ~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| sdtpldt0(xP,xP) = sdtpldt0(xR,xS)
| ~ spl2_33
| ~ spl2_34
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f53658,f26489]) ).
fof(f53660,plain,
( sdtpldt0(xP,xP) = sdtpldt0(xR,xS)
| ~ spl2_33
| ~ spl2_34
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f53659,f218]) ).
fof(f53661,plain,
( $false
| ~ spl2_33
| ~ spl2_34
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f53660,f221]) ).
fof(f53662,plain,
( ~ spl2_33
| ~ spl2_34
| ~ spl2_54 ),
inference(avatar_contradiction_clause,[],[f53661]) ).
cnf(s38,plain,
spl2_33,
inference(sat_conversion,[],[f26498]) ).
cnf(s39,plain,
spl2_34,
inference(sat_conversion,[],[f27070]) ).
cnf(s60,plain,
( spl2_54
| ~ spl2_55
| ~ spl2_56 ),
inference(sat_conversion,[],[f46122]) ).
cnf(s61,plain,
( ~ spl2_33
| spl2_55 ),
inference(sat_conversion,[],[f46159]) ).
cnf(s62,plain,
( ~ spl2_34
| spl2_56 ),
inference(sat_conversion,[],[f47120]) ).
cnf(s72,plain,
( ~ spl2_33
| ~ spl2_34
| ~ spl2_54 ),
inference(sat_conversion,[],[f53662]) ).
cnf(s77,plain,
spl2_56,
inference(rat,[],[s62,s39]) ).
cnf(s78,plain,
~ spl2_54,
inference(rat,[],[s72,s39,s38]) ).
cnf(s79,plain,
spl2_55,
inference(rat,[],[s61,s38]) ).
cnf(s81,plain,
$false,
inference(rat,[],[s60,s77,s79,s78]) ).
fof(f53663,plain,
$false,
inference(avatar_sat_refutation,[],[s81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG073+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/5.39 % Computer : n004.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Sun Sep 27 23:08:27 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/5.42 Running first-order model finding
% 0.14/5.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.20/7.35 % (3991244)Will run a generic schedule for satisfiability detection.
% 13.20/7.35 % (3991253)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2557545886:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.20/7.35 % (3991250)% WARNING: option uhcvi not known.
% 13.20/7.35 % (3991249)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2209358395_2999 on theBenchmark for (2999ds/0Mi)
% 13.20/7.35 % (3991250)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=173486782:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.20/7.35 % (3991255)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4243603890:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.20/7.35 % (3991251)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2304371381:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.20/7.35 % (3991252)dis+10_1_sil=32000:sp=arity:random_seed=1585860820:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.20/7.35 % (3991254)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2298623378:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.20/7.35 % TRYING [1]
% 13.20/7.35 % TRYING [2]
% 13.20/7.35 % TRYING [3]
% 13.20/7.35 % TRYING [4]
% 13.20/7.35 % (3991253)Instruction limit reached!
% 13.20/7.35 % (3991253)------------------------------
% 13.20/7.35 % (3991253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.20/7.35 % (3991253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/7.35 % (3991253)CaDiCaL version: 2.1.3
% 13.20/7.35 % (3991253)Termination reason: Instruction limit
% 13.20/7.35 % (3991253)Termination phase: Saturation
% 13.20/7.35 % (3991253)Time elapsed: 0.037 s
% 13.20/7.35 % (3991253)Peak memory usage: 13 MB
% 13.20/7.35 % (3991253)Instructions burned: 118 (million)
% 13.20/7.35 % (3991263)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=291628563:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.20/7.35 % TRYING [1]
% 13.20/7.35 % TRYING [2]
% 13.20/7.35 % TRYING [3]
% 13.20/7.35 % TRYING [4]
% 13.20/7.35 % (3991252)Instruction limit reached!
% 13.20/7.35 % (3991252)------------------------------
% 13.20/7.35 % (3991252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.20/7.35 % (3991252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/7.35 % (3991252)CaDiCaL version: 2.1.3
% 13.20/7.35 % (3991252)Termination reason: Instruction limit
% 13.20/7.35 % (3991252)Termination phase: Saturation
% 13.20/7.35 % (3991252)Time elapsed: 0.063 s
% 13.20/7.35 % (3991252)Peak memory usage: 12 MB
% 13.20/7.35 % (3991252)Instructions burned: 105 (million)
% 13.20/7.35 % (3991254)Instruction limit reached!
% 13.20/7.35 % (3991254)------------------------------
% 13.20/7.35 % (3991254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.20/7.35 % (3991254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/7.35 % (3991254)CaDiCaL version: 2.1.3
% 13.20/7.35 % (3991254)Termination reason: Instruction limit
% 13.20/7.35 % (3991254)Termination phase: Saturation
% 13.20/7.35 % (3991254)Time elapsed: 0.070 s
% 13.20/7.35 % (3991254)Peak memory usage: 13 MB
% 13.20/7.35 % (3991254)Instructions burned: 131 (million)
% 13.20/7.35 % TRYING [5]
% 13.20/7.35 % (3991265)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1731989054:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.20/7.35 % TRYING [5]
% 13.20/7.35 % (3991266)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=2759664560:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.20/7.35 % (3991255)Instruction limit reached!
% 13.20/7.35 % (3991255)------------------------------
% 13.20/7.35 % (3991255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.20/7.35 % (3991255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/7.35 % (3991255)CaDiCaL version: 2.1.3
% 13.20/7.35 % (3991255)Termination reason: Instruction limit
% 13.20/7.35 % (3991255)Termination phase: Saturation
% 13.20/7.35 % (3991255)Time elapsed: 0.099 s
% 13.20/7.35 % (3991255)Peak memory usage: 14 MB
% 13.20/7.35 % (3991255)Instructions burned: 159 (million)
% 13.20/7.35 % (3991269)ott-21_1_sil=16000:fs=off:random_seed=919325412:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.20/7.35 % (3991265)Instruction limit reached!
% 13.20/7.35 % (3991265)------------------------------
% 13.20/7.35 % (3991265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991265)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991265)Termination reason: Instruction limit
% 15.12/7.67 % (3991265)Termination phase: Saturation
% 15.12/7.67 % (3991265)Time elapsed: 0.059 s
% 15.12/7.67 % (3991265)Peak memory usage: 12 MB
% 15.12/7.67 % (3991265)Instructions burned: 131 (million)
% 15.12/7.67 % (3991271)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=989418796:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 15.12/7.67 % TRYING [6]
% 15.12/7.67 % (3991263)Instruction limit reached!
% 15.12/7.67 % (3991263)------------------------------
% 15.12/7.67 % (3991263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991263)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991263)Termination reason: Instruction limit
% 15.12/7.67 % (3991263)Termination phase: Finite model building constraint generation
% 15.12/7.67 % (3991263)Time elapsed: 0.141 s
% 15.12/7.67 % (3991263)Peak memory usage: 37 MB
% 15.12/7.67 % (3991263)Instructions burned: 715 (million)
% 15.12/7.67 % (3991273)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1069502362:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.12/7.67 % TRYING [1]
% 15.12/7.67 % TRYING [2]
% 15.12/7.67 % (3991269)Instruction limit reached!
% 15.12/7.67 % (3991269)------------------------------
% 15.12/7.67 % (3991269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991269)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991269)Termination reason: Instruction limit
% 15.12/7.67 % (3991269)Termination phase: Saturation
% 15.12/7.67 % (3991269)Time elapsed: 0.086 s
% 15.12/7.67 % (3991269)Peak memory usage: 13 MB
% 15.12/7.67 % (3991269)Instructions burned: 180 (million)
% 15.12/7.67 % TRYING [3]
% 15.12/7.67 % (3991275)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3476088155:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 15.12/7.67 % TRYING [6]
% 15.12/7.67 % TRYING [4]
% 15.12/7.67 % (3991266)Instruction limit reached!
% 15.12/7.67 % (3991266)------------------------------
% 15.12/7.67 % (3991266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991266)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991266)Termination reason: Instruction limit
% 15.12/7.67 % (3991266)Termination phase: Saturation
% 15.12/7.67 % (3991266)Time elapsed: 0.276 s
% 15.12/7.67 % (3991266)Peak memory usage: 14 MB
% 15.12/7.67 % (3991266)Instructions burned: 686 (million)
% 15.12/7.67 % TRYING [5]
% 15.12/7.67 % (3991273)Instruction limit reached!
% 15.12/7.67 % (3991273)------------------------------
% 15.12/7.67 % (3991273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991273)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991273)Termination reason: Instruction limit
% 15.12/7.67 % (3991273)Termination phase: Finite model building constraint generation
% 15.12/7.67 % (3991273)Time elapsed: 0.175 s
% 15.12/7.67 % (3991273)Peak memory usage: 20 MB
% 15.12/7.67 % (3991273)Instructions burned: 872 (million)
% 15.12/7.67 % (3991278)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=489367328: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)
% 15.12/7.67 % (3991277)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1461301528:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 15.12/7.67 % (3991271)Instruction limit reached!
% 15.12/7.67 % (3991271)------------------------------
% 15.12/7.67 % (3991271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991271)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991271)Termination reason: Instruction limit
% 15.12/7.67 % (3991271)Termination phase: Saturation
% 15.12/7.67 % (3991271)Time elapsed: 0.298 s
% 15.12/7.67 % (3991271)Peak memory usage: 14 MB
% 15.12/7.67 % (3991271)Instructions burned: 477 (million)
% 15.12/7.67 % (3991281)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1062172113:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 15.12/7.67 % (3991278)Instruction limit reached!
% 15.12/7.67 % (3991278)------------------------------
% 15.12/7.67 % (3991278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991278)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991278)Termination reason: Instruction limit
% 15.12/7.67 % (3991278)Termination phase: Saturation
% 15.12/7.67 % (3991278)Time elapsed: 0.196 s
% 15.12/7.67 % (3991278)Peak memory usage: 20 MB
% 15.12/7.67 % (3991278)Instructions burned: 694 (million)
% 15.12/7.67 % (3991283)fmb+10_1_sil=64000:random_seed=3202299066:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 15.12/7.67 % TRYING [1]
% 15.12/7.67 % TRYING [2]
% 15.12/7.67 % TRYING [3]
% 15.12/7.67 % TRYING [7]
% 15.12/7.67 % TRYING [4]
% 15.12/7.67 % TRYING [5]
% 15.12/7.67 % (3991277)Instruction limit reached!
% 15.12/7.67 % (3991277)------------------------------
% 15.12/7.67 % (3991277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991277)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991277)Termination reason: Instruction limit
% 15.12/7.67 % (3991277)Termination phase: Finite model building constraint generation
% 15.12/7.67 % (3991277)Time elapsed: 0.409 s
% 15.12/7.67 % (3991277)Peak memory usage: 108 MB
% 15.12/7.67 % (3991277)Instructions burned: 892 (million)
% 15.12/7.67 % (3991285)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1579221251:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 15.12/7.67 % TRYING [20]
% 15.12/7.67 % (3991275)Instruction limit reached!
% 15.12/7.67 % (3991275)------------------------------
% 15.12/7.67 % (3991275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991275)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991275)Termination reason: Instruction limit
% 15.12/7.67 % (3991275)Termination phase: Saturation
% 15.12/7.67 % (3991275)Time elapsed: 0.618 s
% 15.12/7.67 % (3991275)Peak memory usage: 26 MB
% 15.12/7.67 % (3991275)Instructions burned: 1180 (million)
% 15.12/7.67 % (3991287)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=239441441:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 15.12/7.67 % TRYING [8]
% 15.12/7.67 % (3991281)Instruction limit reached!
% 15.12/7.67 % (3991281)------------------------------
% 15.12/7.67 % (3991281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991281)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991281)Termination reason: Instruction limit
% 15.12/7.67 % (3991281)Termination phase: Saturation
% 15.12/7.67 % (3991281)Time elapsed: 0.497 s
% 15.12/7.67 % (3991281)Peak memory usage: 19 MB
% 15.12/7.67 % (3991281)Instructions burned: 879 (million)
% 15.12/7.67 % (3991289)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3708771912:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 15.12/7.67 % (3991287)Instruction limit reached!
% 15.12/7.67 % (3991287)------------------------------
% 15.12/7.67 % (3991287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991287)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991287)Termination reason: Instruction limit
% 15.12/7.67 % (3991287)Termination phase: Finite model building constraint generation
% 15.12/7.67 % (3991287)Time elapsed: 0.304 s
% 15.12/7.67 % (3991287)Peak memory usage: 63 MB
% 15.12/7.67 % (3991287)Instructions burned: 923 (million)
% 15.12/7.67 % TRYING [6]
% 15.12/7.67 % (3991291)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3894376663:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 15.12/7.67 % TRYING [8]
% 15.12/7.67 % (3991291)Instruction limit reached!
% 15.12/7.67 % (3991291)------------------------------
% 15.12/7.67 % (3991291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991291)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991291)Termination reason: Instruction limit
% 15.12/7.67 % (3991291)Termination phase: Saturation
% 15.12/7.67 % (3991291)Time elapsed: 0.668 s
% 15.12/7.67 % (3991291)Peak memory usage: 18 MB
% 15.12/7.67 % (3991291)Instructions burned: 1473 (million)
% 15.12/7.67 % (3991293)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2498687792:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 15.12/7.67 % (3991293)Cannot represent all propositional literals internally
% 15.12/7.67 % (3991293)Refutation not found, incomplete strategy
% 15.12/7.67 % (3991293)------------------------------
% 15.12/7.67 % (3991293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.67 % (3991293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.67 % (3991293)CaDiCaL version: 2.1.3
% 15.12/7.67 % (3991293)Termination reason: Refutation not found, incomplete strategy
% 15.12/7.67 % (3991293)Time elapsed: 0.008 s
% 15.12/7.67 % (3991293)Peak memory usage: 10 MB
% 15.12/7.67 % (3991293)Instructions burned: 15 (million)
% 15.12/7.67 % (3991293)------------------------------
% 15.12/7.67 % (3991293)------------------------------
% 15.12/7.67 % (3991295)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1521970702:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 15.12/7.67 % TRYING [16]
% 15.12/7.67 % (3991289) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3991244-3991289"...
% 15.12/7.67 % (3991289)...printing done.
% 15.12/7.67 % (3991289)Refutation found. Thanks to Tanya!
% 15.12/7.67 % SZS status Theorem for theBenchmark
% 15.12/7.67 % SZS output start Proof for theBenchmark
% See solution above
% 15.12/7.68 % (3991289)------------------------------
% 15.12/7.68 % (3991289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.12/7.68 % (3991289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.12/7.68 % (3991289)CaDiCaL version: 2.1.3
% 15.12/7.68 % (3991289)Termination reason: Refutation
% 15.12/7.68 % (3991289)Time elapsed: 1.171 s
% 15.12/7.68 % (3991289)Peak memory usage: 34 MB
% 15.12/7.68 % (3991289)Instructions burned: 2451 (million)
% 15.12/7.68 % (3991244)Success in time 2.241 s
% 15.12/7.68 % Vampire exiting
%------------------------------------------------------------------------------