%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG061+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 : n001.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:54 PM UTC 2026
% Result : Theorem 83.51s 30.75s
% Output : Refutation 83.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 13
% Syntax : Number of formulae : 62 ( 21 unt; 4 def)
% Number of atoms : 141 ( 31 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 143 ( 64 ~; 56 |; 16 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 30 ( 0 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSZeroSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulSc) ).
fof(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNegSc) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArith) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1892) ).
fof(f54,axiom,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1930) ).
fof(f58,axiom,
( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)
& sdtasdt0(smndt0(xS),xR) = smndt0(xN)
& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2144) ).
fof(f59,axiom,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2180) ).
fof(f60,conjecture,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f61,negated_conjecture,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(negated_conjecture,[status(cth)],[f60]) ).
fof(f67,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(flattening,[],[f61]) ).
fof(f76,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f77,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f80]) ).
fof(f134,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f136,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f137,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f148,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f81]) ).
fof(f204,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f208,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f213,plain,
sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS),
inference(cnf_transformation,[],[f58]) ).
fof(f215,plain,
sdtasdt0(xR,smndt0(xS)) = smndt0(xN),
inference(cnf_transformation,[],[f58]) ).
fof(f216,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))),
inference(cnf_transformation,[],[f59]) ).
fof(f217,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))),
inference(cnf_transformation,[],[f67]) ).
fof(f237,definition,
( spl2_5
<=> ! [X0] : ~ aScalar0(X0) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f238,plain,
( ! [X0] : ~ aScalar0(X0)
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( $false
| ~ spl2_5 ),
inference(resolution,[],[f238,f134]) ).
fof(f265,plain,
~ spl2_5,
inference(avatar_contradiction_clause,[],[f239]) ).
fof(f3794,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS))
| ~ aScalar0(smndt0(xS)) ),
inference(superposition,[],[f136,f213]) ).
fof(f3803,plain,
( aScalar0(smndt0(xN))
| ~ aScalar0(xR)
| ~ aScalar0(smndt0(xS)) ),
inference(superposition,[],[f136,f215]) ).
fof(f3806,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ aScalar0(smndt0(xS)) ),
inference(duplicate_literal_removal,[],[f3794]) ).
fof(f3807,plain,
( aScalar0(smndt0(xN))
| ~ aScalar0(smndt0(xS)) ),
inference(forward_subsumption_resolution,[],[f3803,f204]) ).
fof(f4584,definition,
( spl2_93
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f4585,plain,
( ! [X0,X1] :
( ~ aScalar0(X1)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0) )
| ~ spl2_93 ),
inference(avatar_component_clause,[],[f4584]) ).
fof(f4586,plain,
( spl2_5
| spl2_93 ),
inference(avatar_split_clause,[],[f148,f4584,f237]) ).
fof(f5107,definition,
( spl2_107
<=> aScalar0(smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_107])],[avatar_definition]) ).
fof(f5108,plain,
( aScalar0(smndt0(xS))
| ~ spl2_107 ),
inference(avatar_component_clause,[],[f5107]) ).
fof(f5109,plain,
( ~ aScalar0(smndt0(xS))
| spl2_107 ),
inference(avatar_component_clause,[],[f5107]) ).
fof(f5111,definition,
( spl2_108
<=> aScalar0(smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl2_108])],[avatar_definition]) ).
fof(f5113,plain,
( aScalar0(smndt0(xN))
| ~ spl2_108 ),
inference(avatar_component_clause,[],[f5111]) ).
fof(f5114,plain,
( ~ spl2_107
| spl2_108 ),
inference(avatar_split_clause,[],[f3807,f5111,f5107]) ).
fof(f5115,plain,
( ~ aScalar0(xS)
| spl2_107 ),
inference(resolution,[],[f5109,f137]) ).
fof(f5116,plain,
( $false
| spl2_107 ),
inference(forward_subsumption_resolution,[],[f5115,f208]) ).
fof(f5117,plain,
spl2_107,
inference(avatar_contradiction_clause,[],[f5116]) ).
fof(f5145,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,smndt0(xN)) = sdtpldt0(smndt0(xN),X0) )
| ~ spl2_93
| ~ spl2_108 ),
inference(resolution,[],[f5113,f4585]) ).
fof(f5158,plain,
( aScalar0(sdtasdt0(xS,xS))
| ~ spl2_107 ),
inference(forward_subsumption_resolution,[],[f3806,f5108]) ).
fof(f5214,plain,
( sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)) = sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))
| ~ spl2_93
| ~ spl2_107
| ~ spl2_108 ),
inference(resolution,[],[f5145,f5158]) ).
fof(f24302,plain,
( sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS)))
| ~ spl2_93
| ~ spl2_107
| ~ spl2_108 ),
inference(superposition,[],[f217,f5214]) ).
fof(f24304,plain,
( $false
| ~ spl2_93
| ~ spl2_107
| ~ spl2_108 ),
inference(forward_subsumption_resolution,[],[f24302,f216]) ).
fof(f24305,plain,
( ~ spl2_93
| ~ spl2_107
| ~ spl2_108 ),
inference(avatar_contradiction_clause,[],[f24304]) ).
cnf(s156,plain,
~ spl2_5,
inference(sat_conversion,[],[f265]) ).
cnf(s1687,plain,
( spl2_5
| spl2_93 ),
inference(sat_conversion,[],[f4586]) ).
cnf(s1934,plain,
( ~ spl2_107
| spl2_108 ),
inference(sat_conversion,[],[f5114]) ).
cnf(s1937,plain,
spl2_107,
inference(sat_conversion,[],[f5117]) ).
cnf(s5125,plain,
( ~ spl2_93
| ~ spl2_107
| ~ spl2_108 ),
inference(sat_conversion,[],[f24305]) ).
cnf(s5131,plain,
spl2_108,
inference(rat,[],[s1934,s1937]) ).
cnf(s5132,plain,
~ spl2_93,
inference(rat,[],[s5125,s1937,s5131]) ).
cnf(s5133,plain,
spl2_5,
inference(rat,[],[s1687,s5132]) ).
cnf(s5148,plain,
$false,
inference(rat,[],[s156,s5133]) ).
fof(f24306,plain,
$false,
inference(avatar_sat_refutation,[],[s5148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG061+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n001.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 23:10:02 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/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
% 14.65/2.52 % (4076121)Will run a generic schedule for satisfiability detection.
% 14.65/2.52 % (4076126)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=12607350_2999 on theBenchmark for (2999ds/0Mi)
% 14.65/2.52 % (4076127)% WARNING: option uhcvi not known.
% 14.65/2.52 % TRYING [1]
% 14.65/2.52 % TRYING [2]
% 14.65/2.52 % TRYING [3]
% 14.65/2.52 % (4076129)dis+10_1_sil=32000:sp=arity:random_seed=3584240199:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.65/2.52 % (4076127)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=713617599:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.65/2.52 % (4076131)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1622095342:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.65/2.52 % (4076128)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2417381758:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.65/2.52 % (4076130)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3221461196:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.65/2.52 % (4076132)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1572082157:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.65/2.52 % TRYING [4]
% 14.65/2.52 % TRYING [5]
% 14.65/2.52 % (4076129)Instruction limit reached!
% 14.65/2.52 % (4076129)------------------------------
% 14.65/2.52 % (4076129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.65/2.52 % (4076129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/2.52 % (4076129)CaDiCaL version: 2.1.3
% 14.65/2.52 % (4076129)Termination reason: Instruction limit
% 14.65/2.52 % (4076129)Termination phase: Saturation
% 14.65/2.52 % (4076129)Time elapsed: 0.062 s
% 14.65/2.52 % (4076129)Peak memory usage: 13 MB
% 14.65/2.52 % (4076129)Instructions burned: 105 (million)
% 14.65/2.52 % (4076130)Instruction limit reached!
% 14.65/2.52 % (4076130)------------------------------
% 14.65/2.52 % (4076130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.65/2.52 % (4076130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/2.52 % (4076130)CaDiCaL version: 2.1.3
% 14.65/2.52 % (4076130)Termination reason: Instruction limit
% 14.65/2.52 % (4076130)Termination phase: Saturation
% 14.65/2.52 % (4076130)Time elapsed: 0.067 s
% 14.65/2.52 % (4076130)Peak memory usage: 13 MB
% 14.65/2.52 % (4076130)Instructions burned: 119 (million)
% 14.65/2.52 % (4076131)Instruction limit reached!
% 14.65/2.52 % (4076131)------------------------------
% 14.65/2.52 % (4076131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.65/2.52 % (4076131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/2.52 % (4076131)CaDiCaL version: 2.1.3
% 14.65/2.52 % (4076131)Termination reason: Instruction limit
% 14.65/2.52 % (4076131)Termination phase: Saturation
% 14.65/2.52 % (4076131)Time elapsed: 0.071 s
% 14.65/2.52 % (4076131)Peak memory usage: 13 MB
% 14.65/2.52 % (4076131)Instructions burned: 132 (million)
% 14.65/2.52 % (4076140)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=905682090:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.65/2.52 % (4076141)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=955168703:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.65/2.52 % (4076142)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=2568752829:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.65/2.52 % TRYING [1]
% 14.65/2.52 % TRYING [2]
% 14.65/2.52 % (4076132)Instruction limit reached!
% 14.65/2.52 % (4076132)------------------------------
% 14.65/2.52 % (4076132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.65/2.52 % (4076132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/2.52 % (4076132)CaDiCaL version: 2.1.3
% 14.65/2.52 % (4076132)Termination reason: Instruction limit
% 14.65/2.52 % (4076132)Termination phase: Saturation
% 14.65/2.52 % (4076132)Time elapsed: 0.095 s
% 14.65/2.52 % (4076132)Peak memory usage: 15 MB
% 14.65/2.52 % (4076132)Instructions burned: 159 (million)
% 14.65/2.52 % TRYING [3]
% 14.65/2.52 % TRYING [4]
% 14.65/2.52 % (4076146)ott-21_1_sil=16000:fs=off:random_seed=3991516652:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.65/2.52 % TRYING [6]
% 14.65/2.52 % (4076141)Instruction limit reached!
% 14.65/2.52 % (4076141)------------------------------
% 14.65/2.52 % (4076141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076141)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076141)Termination reason: Instruction limit
% 41.58/6.33 % (4076141)Termination phase: Saturation
% 41.58/6.33 % (4076141)Time elapsed: 0.060 s
% 41.58/6.33 % (4076141)Peak memory usage: 12 MB
% 41.58/6.33 % (4076141)Instructions burned: 133 (million)
% 41.58/6.33 % (4076148)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2150802215:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.58/6.33 % TRYING [5]
% 41.58/6.33 % (4076146)Instruction limit reached!
% 41.58/6.33 % (4076146)------------------------------
% 41.58/6.33 % (4076146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076146)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076146)Termination reason: Instruction limit
% 41.58/6.33 % (4076146)Termination phase: Saturation
% 41.58/6.33 % (4076146)Time elapsed: 0.087 s
% 41.58/6.33 % (4076146)Peak memory usage: 13 MB
% 41.58/6.33 % (4076146)Instructions burned: 180 (million)
% 41.58/6.33 % (4076150)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4118351093:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.58/6.33 % TRYING [1]
% 41.58/6.33 % TRYING [2]
% 41.58/6.33 % TRYING [3]
% 41.58/6.33 % TRYING [4]
% 41.58/6.33 % TRYING [6]
% 41.58/6.33 % TRYING [7]
% 41.58/6.33 % (4076140)Instruction limit reached!
% 41.58/6.33 % (4076140)------------------------------
% 41.58/6.33 % (4076140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076140)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076140)Termination reason: Instruction limit
% 41.58/6.33 % (4076140)Termination phase: Finite model building constraint generation
% 41.58/6.33 % (4076140)Time elapsed: 0.260 s
% 41.58/6.33 % (4076140)Peak memory usage: 37 MB
% 41.58/6.33 % (4076140)Instructions burned: 714 (million)
% 41.58/6.33 % (4076152)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2975962718:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 41.58/6.33 % (4076148)Instruction limit reached!
% 41.58/6.33 % (4076148)------------------------------
% 41.58/6.33 % (4076148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076148)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076148)Termination reason: Instruction limit
% 41.58/6.33 % (4076148)Termination phase: Saturation
% 41.58/6.33 % (4076148)Time elapsed: 0.297 s
% 41.58/6.33 % (4076148)Peak memory usage: 15 MB
% 41.58/6.33 % (4076148)Instructions burned: 477 (million)
% 41.58/6.33 % (4076142)Instruction limit reached!
% 41.58/6.33 % (4076142)------------------------------
% 41.58/6.33 % (4076142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076142)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076142)Termination reason: Instruction limit
% 41.58/6.33 % (4076142)Termination phase: Saturation
% 41.58/6.33 % (4076142)Time elapsed: 0.387 s
% 41.58/6.33 % (4076142)Peak memory usage: 20 MB
% 41.58/6.33 % (4076142)Instructions burned: 684 (million)
% 41.58/6.33 % (4076154)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3438841328:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.58/6.33 % (4076155)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=2041151783: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)
% 41.58/6.33 % TRYING [5]
% 41.58/6.33 % (4076150)Instruction limit reached!
% 41.58/6.33 % (4076150)------------------------------
% 41.58/6.33 % (4076150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.58/6.33 % (4076150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.58/6.33 % (4076150)CaDiCaL version: 2.1.3
% 41.58/6.33 % (4076150)Termination reason: Instruction limit
% 41.58/6.33 % (4076150)Termination phase: Finite model building constraint generation
% 41.58/6.33 % (4076150)Time elapsed: 0.332 s
% 41.58/6.33 % (4076150)Peak memory usage: 20 MB
% 41.58/6.33 % (4076150)Instructions burned: 867 (million)
% 41.58/6.33 % (4076158)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2962136158:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.58/6.33 % (4076155)Instruction limit reached!
% 92.65/13.50 % (4076155)------------------------------
% 92.65/13.50 % (4076155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076155)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076155)Termination reason: Instruction limit
% 92.65/13.50 % (4076155)Termination phase: Saturation
% 92.65/13.50 % (4076155)Time elapsed: 0.328 s
% 92.65/13.50 % (4076155)Peak memory usage: 21 MB
% 92.65/13.50 % (4076155)Instructions burned: 692 (million)
% 92.65/13.50 % (4076160)fmb+10_1_sil=64000:random_seed=2306293421:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 92.65/13.50 % TRYING [1]
% 92.65/13.50 % TRYING [2]
% 92.65/13.50 % TRYING [3]
% 92.65/13.50 % TRYING [8]
% 92.65/13.50 % (4076154)Instruction limit reached!
% 92.65/13.50 % (4076154)------------------------------
% 92.65/13.50 % (4076154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076154)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076154)Termination reason: Instruction limit
% 92.65/13.50 % (4076154)Termination phase: Finite model building constraint generation
% 92.65/13.50 % (4076154)Time elapsed: 0.402 s
% 92.65/13.50 % (4076154)Peak memory usage: 104 MB
% 92.65/13.50 % (4076154)Instructions burned: 890 (million)
% 92.65/13.50 % (4076162)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2869302537:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 92.65/13.50 % TRYING [20]
% 92.65/13.50 % TRYING [4]
% 92.65/13.50 % (4076152)Instruction limit reached!
% 92.65/13.50 % (4076152)------------------------------
% 92.65/13.50 % (4076152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076152)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076152)Termination reason: Instruction limit
% 92.65/13.50 % (4076152)Termination phase: Saturation
% 92.65/13.50 % (4076152)Time elapsed: 0.623 s
% 92.65/13.50 % (4076152)Peak memory usage: 29 MB
% 92.65/13.50 % (4076152)Instructions burned: 1179 (million)
% 92.65/13.50 % (4076164)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1090315603:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 92.65/13.50 % TRYING [8]
% 92.65/13.50 % (4076158)Instruction limit reached!
% 92.65/13.50 % (4076158)------------------------------
% 92.65/13.50 % (4076158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076158)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076158)Termination reason: Instruction limit
% 92.65/13.50 % (4076158)Termination phase: Saturation
% 92.65/13.50 % (4076158)Time elapsed: 0.507 s
% 92.65/13.50 % (4076158)Peak memory usage: 21 MB
% 92.65/13.50 % (4076158)Instructions burned: 881 (million)
% 92.65/13.50 % (4076166)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=857703958:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 92.65/13.50 % TRYING [5]
% 92.65/13.50 % (4076164)Instruction limit reached!
% 92.65/13.50 % (4076164)------------------------------
% 92.65/13.50 % (4076164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076164)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076164)Termination reason: Instruction limit
% 92.65/13.50 % (4076164)Termination phase: Finite model building constraint generation
% 92.65/13.50 % (4076164)Time elapsed: 0.306 s
% 92.65/13.50 % (4076164)Peak memory usage: 63 MB
% 92.65/13.50 % (4076164)Instructions burned: 922 (million)
% 92.65/13.50 % (4076168)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2351178415:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 92.65/13.50 % TRYING [6]
% 92.65/13.50 % TRYING [9]
% 92.65/13.50 % (4076168)Instruction limit reached!
% 92.65/13.50 % (4076168)------------------------------
% 92.65/13.50 % (4076168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.65/13.50 % (4076168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.65/13.50 % (4076168)CaDiCaL version: 2.1.3
% 92.65/13.50 % (4076168)Termination reason: Instruction limit
% 92.65/13.50 % (4076168)Termination phase: Saturation
% 92.65/13.50 % (4076168)Time elapsed: 0.688 s
% 92.65/13.50 % (4076168)Peak memory usage: 19 MB
% 92.65/13.50 % (4076168)Instructions burned: 1472 (million)
% 92.65/13.50 % (4076170)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2342352070:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 83.51/30.75 % (4076170)Cannot represent all propositional literals internally
% 83.51/30.75 % (4076170)Refutation not found, incomplete strategy
% 83.51/30.75 % (4076170)------------------------------
% 83.51/30.75 % (4076170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076170)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076170)Termination reason: Refutation not found, incomplete strategy
% 83.51/30.75 % (4076170)Time elapsed: 0.008 s
% 83.51/30.75 % (4076170)Peak memory usage: 11 MB
% 83.51/30.75 % (4076170)Instructions burned: 15 (million)
% 83.51/30.75 % (4076170)------------------------------
% 83.51/30.75 % (4076170)------------------------------
% 83.51/30.75 % (4076172)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=808512310:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 83.51/30.75 % TRYING [16]
% 83.51/30.75 % (4076172)Instruction limit reached!
% 83.51/30.75 % (4076172)------------------------------
% 83.51/30.75 % (4076172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076172)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076172)Termination reason: Instruction limit
% 83.51/30.75 % (4076172)Termination phase: Finite model building constraint generation
% 83.51/30.75 % (4076172)Time elapsed: 0.760 s
% 83.51/30.75 % (4076172)Peak memory usage: 146 MB
% 83.51/30.75 % (4076172)Instructions burned: 2174 (million)
% 83.51/30.75 % (4076175)ott-2_1_sil=16000:newcnf=on:random_seed=751236036:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 83.51/30.75 % (4076175)Instruction limit reached!
% 83.51/30.75 % (4076175)------------------------------
% 83.51/30.75 % (4076175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076175)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076175)Termination reason: Instruction limit
% 83.51/30.75 % (4076175)Termination phase: Saturation
% 83.51/30.75 % (4076175)Time elapsed: 0.440 s
% 83.51/30.75 % (4076175)Peak memory usage: 25 MB
% 83.51/30.75 % (4076175)Instructions burned: 870 (million)
% 83.51/30.75 % (4076177)ott+10_1_sil=32000:tgt=ground:random_seed=527101102:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 83.51/30.75 % (4076166)Instruction limit reached!
% 83.51/30.75 % (4076166)------------------------------
% 83.51/30.75 % (4076166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076166)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076166)Termination reason: Instruction limit
% 83.51/30.75 % (4076166)Termination phase: Saturation
% 83.51/30.75 % (4076166)Time elapsed: 2.476 s
% 83.51/30.75 % (4076166)Peak memory usage: 58 MB
% 83.51/30.75 % (4076166)Instructions burned: 5132 (million)
% 83.51/30.75 % (4076179)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3472855311:i=54282_2963 on theBenchmark for (2963ds/54282Mi)
% 83.51/30.75 % TRYING [1]
% 83.51/30.75 % TRYING [2]
% 83.51/30.75 % TRYING [3]
% 83.51/30.75 % TRYING [4]
% 83.51/30.75 % TRYING [5]
% 83.51/30.75 % TRYING [6]
% 83.51/30.75 % (4076162)Instruction limit reached!
% 83.51/30.75 % (4076162)------------------------------
% 83.51/30.75 % (4076162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076162)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076162)Termination reason: Instruction limit
% 83.51/30.75 % (4076162)Termination phase: Finite model building constraint generation
% 83.51/30.75 % (4076162)Time elapsed: 3.066 s
% 83.51/30.75 % (4076162)Peak memory usage: 483 MB
% 83.51/30.75 % (4076162)Instructions burned: 9516 (million)
% 83.51/30.75 % (4076181)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1721099462:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 83.51/30.75 % TRYING [7]
% 83.51/30.75 % TRYING [7]
% 83.51/30.75 % TRYING [10]
% 83.51/30.75 % TRYING [8]
% 83.51/30.75 % (4076181)Instruction limit reached!
% 83.51/30.75 % (4076181)------------------------------
% 83.51/30.75 % (4076181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076181)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076181)Termination reason: Instruction limit
% 83.51/30.75 % (4076181)Termination phase: Saturation
% 83.51/30.75 % (4076181)Time elapsed: 1.806 s
% 83.51/30.75 % (4076181)Peak memory usage: 42 MB
% 83.51/30.75 % (4076181)Instructions burned: 3512 (million)
% 83.51/30.75 % (4076183)dis+21_1_sil=32000:sas=cadical:random_seed=1095417451:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 83.51/30.75 % (4076177)Instruction limit reached!
% 83.51/30.75 % (4076177)------------------------------
% 83.51/30.75 % (4076177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076177)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076177)Termination reason: Instruction limit
% 83.51/30.75 % (4076177)Termination phase: Saturation
% 83.51/30.75 % (4076177)Time elapsed: 2.790 s
% 83.51/30.75 % (4076177)Peak memory usage: 75 MB
% 83.51/30.75 % (4076177)Instructions burned: 5114 (million)
% 83.51/30.75 % (4076185)ott+11_1_sil=16000:gs=on:random_seed=2524694730:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2938 on theBenchmark for (2938ds/2251Mi)
% 83.51/30.75 % (4076185)Instruction limit reached!
% 83.51/30.75 % (4076185)------------------------------
% 83.51/30.75 % (4076185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076185)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076185)Termination reason: Instruction limit
% 83.51/30.75 % (4076185)Termination phase: Saturation
% 83.51/30.75 % (4076185)Time elapsed: 0.905 s
% 83.51/30.75 % (4076185)Peak memory usage: 16 MB
% 83.51/30.75 % (4076185)Instructions burned: 2251 (million)
% 83.51/30.75 % (4076187)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1367490228:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi)
% 83.51/30.75 % TRYING [7]
% 83.51/30.75 % TRYING [9]
% 83.51/30.75 % (4076183)Instruction limit reached!
% 83.51/30.75 % (4076183)------------------------------
% 83.51/30.75 % (4076183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076183)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076183)Termination reason: Instruction limit
% 83.51/30.75 % (4076183)Termination phase: Saturation
% 83.51/30.75 % (4076183)Time elapsed: 2.015 s
% 83.51/30.75 % (4076183)Peak memory usage: 44 MB
% 83.51/30.75 % (4076183)Instructions burned: 3774 (million)
% 83.51/30.75 % (4076189)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=998220262:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 83.51/30.75 % (4076160)Instruction limit reached!
% 83.51/30.75 % (4076160)------------------------------
% 83.51/30.75 % (4076160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076160)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076160)Termination reason: Instruction limit
% 83.51/30.75 % (4076160)Termination phase: Finite model building SAT solving
% 83.51/30.75 % (4076160)Time elapsed: 7.902 s
% 83.51/30.75 % (4076160)Peak memory usage: 152 MB
% 83.51/30.75 % (4076160)Instructions burned: 22063 (million)
% 83.51/30.75 % (4076191)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=964364980:i=29340_2911 on theBenchmark for (2911ds/29340Mi)
% 83.51/30.75 % (4076189)Instruction limit reached!
% 83.51/30.75 % (4076189)------------------------------
% 83.51/30.75 % (4076189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076189)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076189)Termination reason: Instruction limit
% 83.51/30.75 % (4076189)Termination phase: Saturation
% 83.51/30.75 % (4076189)Time elapsed: 2.315 s
% 83.51/30.75 % (4076189)Peak memory usage: 65 MB
% 83.51/30.75 % (4076189)Instructions burned: 4593 (million)
% 83.51/30.75 % (4076193)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=317484187:i=5211_2897 on theBenchmark for (2897ds/5211Mi)
% 83.51/30.75 % TRYING [8]
% 83.51/30.75 % TRYING [10]
% 83.51/30.75 % (4076193)Instruction limit reached!
% 83.51/30.75 % (4076193)------------------------------
% 83.51/30.75 % (4076193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076193)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076193)Termination reason: Instruction limit
% 83.51/30.75 % (4076193)Termination phase: Saturation
% 83.51/30.75 % (4076193)Time elapsed: 2.750 s
% 83.51/30.75 % (4076193)Peak memory usage: 60 MB
% 83.51/30.75 % (4076193)Instructions burned: 5215 (million)
% 83.51/30.75 % (4076200)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3299110438:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi)
% 83.51/30.75 % TRYING [17]
% 83.51/30.75 % TRYING [11]
% 83.51/30.75 % (4076200)Instruction limit reached!
% 83.51/30.75 % (4076200)------------------------------
% 83.51/30.75 % (4076200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076200)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076200)Termination reason: Instruction limit
% 83.51/30.75 % (4076200)Termination phase: Finite model building constraint generation
% 83.51/30.75 % (4076200)Time elapsed: 2.021 s
% 83.51/30.75 % (4076200)Peak memory usage: 309 MB
% 83.51/30.75 % (4076200)Instructions burned: 5498 (million)
% 83.51/30.75 % (4076463)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=362213507:fmbsr=2:i=46332_2848 on theBenchmark for (2848ds/46332Mi)
% 83.51/30.75 % TRYING [15]
% 83.51/30.75 % TRYING [9]
% 83.51/30.75 % (4076191)Instruction limit reached!
% 83.51/30.75 % (4076191)------------------------------
% 83.51/30.75 % (4076191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076191)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076191)Termination reason: Instruction limit
% 83.51/30.75 % (4076191)Termination phase: Saturation
% 83.51/30.75 % (4076191)Time elapsed: 15.327 s
% 83.51/30.75 % (4076191)Peak memory usage: 347 MB
% 83.51/30.75 % (4076191)Instructions burned: 29340 (million)
% 83.51/30.75 % (4076648)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2733894977:i=14071_2758 on theBenchmark for (2758ds/14071Mi)
% 83.51/30.75 % TRYING [12]
% 83.51/30.75 % (4076648)Instruction limit reached!
% 83.51/30.75 % (4076648)------------------------------
% 83.51/30.75 % (4076648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076648)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076648)Termination reason: Instruction limit
% 83.51/30.75 % (4076648)Termination phase: Finite model building constraint generation
% 83.51/30.75 % (4076648)Time elapsed: 5.074 s
% 83.51/30.75 % (4076648)Peak memory usage: 965 MB
% 83.51/30.75 % (4076648)Instructions burned: 14071 (million)
% 83.51/30.75 % (4076179)Instruction limit reached!
% 83.51/30.75 % (4076179)------------------------------
% 83.51/30.75 % (4076179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076179)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076179)Termination reason: Instruction limit
% 83.51/30.75 % (4076179)Termination phase: Finite model building SAT solving
% 83.51/30.75 % (4076179)Time elapsed: 25.727 s
% 83.51/30.75 % (4076179)Peak memory usage: 1395 MB
% 83.51/30.75 % (4076179)Instructions burned: 54283 (million)
% 83.51/30.75 % (4076897)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3352187544:i=22565:add=on:rawr=on_2705 on theBenchmark for (2705ds/22565Mi)
% 83.51/30.75 % (4076899)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2278005228:i=8173:av=off_2704 on theBenchmark for (2704ds/8173Mi)
% 83.51/30.75 % (4076897) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4076121-4076897"...
% 83.51/30.75 % (4076897)...printing done.
% 83.51/30.75 % (4076897)Refutation found. Thanks to Tanya!
% 83.51/30.75 % SZS status Theorem for theBenchmark
% 83.51/30.75 % SZS output start Proof for theBenchmark
% See solution above
% 83.51/30.75 % (4076897)------------------------------
% 83.51/30.75 % (4076897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.51/30.75 % (4076897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.51/30.75 % (4076897)CaDiCaL version: 2.1.3
% 83.51/30.75 % (4076897)Termination reason: Refutation
% 83.51/30.75 % (4076897)Time elapsed: 0.462 s
% 83.51/30.75 % (4076897)Peak memory usage: 22 MB
% 83.51/30.75 % (4076897)Instructions burned: 866 (million)
% 83.51/30.75 % (4076121)Success in time 30.318 s
% 83.51/30.75 % Vampire exiting
%------------------------------------------------------------------------------