%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR089+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 09:45:07 AM UTC 2026
% Result : Theorem 228.45s 32.90s
% Output : Refutation 228.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 14
% Syntax : Number of formulae : 75 ( 23 unt; 2 def)
% Number of atoms : 210 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 245 ( 110 ~; 99 |; 16 &)
% ( 6 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 3 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 69 ( 0 sgn 65 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X1,X0] :
( s__subclass(X0,X1)
=> ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X1,X2,X0] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
=> ( ( s__instance(X2,X0)
& s__subclass(X0,X1) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f55,axiom,
! [X1,X0] :
( ( s__instance(X0,s__EngineeringComponent)
& s__instance(X1,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X0,X1)
=> s__connected(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_55) ).
fof(f4643,axiom,
! [X0,X1] :
( ( s__instance(X1,s__Object)
& s__instance(X0,s__Object) )
=> ( s__connected(X0,X1)
=> ( s__overlapsSpatially(X0,X1)
| s__meetsSpatially(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_4658) ).
fof(f6441,axiom,
! [X1,X0] :
( ( s__instance(X1,s__EngineeringComponent)
& s__instance(X0,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X1,X0)
<=> ? [X2] :
( s__connectsEngineeringComponents(X2,X1,X0)
& s__instance(X2,s__EngineeringConnection) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6522) ).
fof(f12483,axiom,
s__subclass(s__EngineeringComponent,s__Object),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+3.ax',kb_SUMOcache_5266) ).
fof(f14788,axiom,
s__instance(s__Object16_1,s__EngineeringConnection),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f14789,axiom,
s__instance(s__Object16_2,s__EngineeringComponent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f14790,axiom,
s__instance(s__Object16_3,s__EngineeringComponent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f14791,axiom,
s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(f14792,axiom,
~ s__overlapsSpatially(s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(f14793,conjecture,
s__meetsSpatially(s__Object16_2,s__Object16_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f14794,negated_conjecture,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(negated_conjecture,[status(cth)],[f14793]) ).
fof(f15101,plain,
! [X2,X1,X0] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X2,s__SetOrClass) )
=> ( ( s__subclass(X2,X0)
& s__instance(X1,X2) )
=> s__instance(X1,X0) ) ),
inference(rectify,[],[f27]) ).
fof(f15420,plain,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(flattening,[],[f14794]) ).
fof(f15604,plain,
! [X1,X0] :
( ( s__instance(X1,s__EngineeringComponent)
& s__instance(X0,s__EngineeringComponent) )
=> ( s__connectedEngineeringComponents(X1,X0)
=> s__connected(X1,X0) ) ),
inference(rectify,[],[f55]) ).
fof(f15637,plain,
! [X1,X0] :
( ( s__instance(X0,s__EngineeringComponent)
& s__instance(X1,s__EngineeringComponent) )
=> ( ? [X2] :
( s__connectsEngineeringComponents(X2,X0,X1)
& s__instance(X2,s__EngineeringConnection) )
<=> s__connectedEngineeringComponents(X0,X1) ) ),
inference(rectify,[],[f6441]) ).
fof(f15998,plain,
! [X0,X1] :
( s__subclass(X1,X0)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
inference(rectify,[],[f26]) ).
fof(f16122,plain,
! [X2,X1,X0] :
( s__instance(X1,X0)
| ~ s__subclass(X2,X0)
| ~ s__instance(X1,X2)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
inference(ennf_transformation,[],[f15101]) ).
fof(f16123,plain,
! [X2,X0,X1] :
( s__instance(X1,X0)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__subclass(X2,X0)
| ~ s__instance(X1,X2)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f16122]) ).
fof(f16452,plain,
! [X0,X1] :
( s__overlapsSpatially(X0,X1)
| s__meetsSpatially(X0,X1)
| ~ s__connected(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f4643]) ).
fof(f16453,plain,
! [X0,X1] :
( s__meetsSpatially(X0,X1)
| ~ s__instance(X0,s__Object)
| s__overlapsSpatially(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__connected(X0,X1) ),
inference(flattening,[],[f16452]) ).
fof(f17078,plain,
! [X1,X0] :
( ( ? [X2] :
( s__connectsEngineeringComponents(X2,X0,X1)
& s__instance(X2,s__EngineeringConnection) )
<=> s__connectedEngineeringComponents(X0,X1) )
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(ennf_transformation,[],[f15637]) ).
fof(f17079,plain,
! [X0,X1] :
( ( ? [X2] :
( s__connectsEngineeringComponents(X2,X0,X1)
& s__instance(X2,s__EngineeringConnection) )
<=> s__connectedEngineeringComponents(X0,X1) )
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(flattening,[],[f17078]) ).
fof(f17825,plain,
! [X1,X0] :
( s__connected(X1,X0)
| ~ s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(ennf_transformation,[],[f15604]) ).
fof(f17826,plain,
! [X1,X0] :
( s__connected(X1,X0)
| ~ s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(flattening,[],[f17825]) ).
fof(f21173,plain,
! [X1,X0] :
( ~ s__subclass(X1,X0)
| ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
inference(ennf_transformation,[],[f15998]) ).
fof(f21264,plain,
s__subclass(s__EngineeringComponent,s__Object),
inference(cnf_transformation,[],[f12483]) ).
fof(f23520,plain,
~ s__overlapsSpatially(s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f14792]) ).
fof(f23664,plain,
s__instance(s__Object16_1,s__EngineeringConnection),
inference(cnf_transformation,[],[f14788]) ).
fof(f26881,plain,
! [X2,X0,X1] :
( s__connectedEngineeringComponents(X0,X1)
| ~ s__instance(X2,s__EngineeringConnection)
| ~ s__instance(X0,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X2,X0,X1)
| ~ s__instance(X1,s__EngineeringComponent) ),
inference(cnf_transformation,[],[f17079]) ).
fof(f26911,plain,
s__instance(s__Object16_2,s__EngineeringComponent),
inference(cnf_transformation,[],[f14789]) ).
fof(f27312,plain,
! [X0,X1] :
( s__connected(X1,X0)
| ~ s__connectedEngineeringComponents(X1,X0)
| ~ s__instance(X1,s__EngineeringComponent)
| ~ s__instance(X0,s__EngineeringComponent) ),
inference(cnf_transformation,[],[f17826]) ).
fof(f29215,plain,
s__instance(s__Object16_3,s__EngineeringComponent),
inference(cnf_transformation,[],[f14790]) ).
fof(f31783,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X0) ),
inference(cnf_transformation,[],[f21173]) ).
fof(f31784,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X1,X0) ),
inference(cnf_transformation,[],[f21173]) ).
fof(f34460,plain,
! [X0,X1] :
( s__meetsSpatially(X0,X1)
| s__overlapsSpatially(X0,X1)
| ~ s__instance(X1,s__Object)
| ~ s__connected(X0,X1)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f16453]) ).
fof(f35360,plain,
~ s__meetsSpatially(s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f15420]) ).
fof(f35927,plain,
! [X2,X0,X1] :
( ~ s__subclass(X2,X0)
| ~ s__instance(X0,s__SetOrClass)
| s__instance(X1,X0)
| ~ s__instance(X1,X2)
| ~ s__instance(X2,s__SetOrClass) ),
inference(cnf_transformation,[],[f16123]) ).
fof(f36054,plain,
s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3),
inference(cnf_transformation,[],[f14791]) ).
fof(f50343,definition,
( spl478_163
<=> s__instance(s__Object16_2,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_163])],[avatar_definition]) ).
fof(f50344,plain,
( s__instance(s__Object16_2,s__Object)
| ~ spl478_163 ),
inference(avatar_component_clause,[],[f50343]) ).
fof(f50345,plain,
( ~ s__instance(s__Object16_2,s__Object)
| spl478_163 ),
inference(avatar_component_clause,[],[f50343]) ).
fof(f50351,definition,
( spl478_165
<=> s__instance(s__Object16_3,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_165])],[avatar_definition]) ).
fof(f50352,plain,
( s__instance(s__Object16_3,s__Object)
| ~ spl478_165 ),
inference(avatar_component_clause,[],[f50351]) ).
fof(f50353,plain,
( ~ s__instance(s__Object16_3,s__Object)
| spl478_165 ),
inference(avatar_component_clause,[],[f50351]) ).
fof(f91981,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_2,s__Object)
| s__overlapsSpatially(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__Object) ),
inference(resolution,[],[f34460,f35360]) ).
fof(f95375,plain,
! [X2,X0,X1] :
( ~ s__instance(X1,X2)
| s__instance(X1,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X2,X0) ),
inference(forward_subsumption_resolution,[],[f35927,f31783]) ).
fof(f95376,plain,
! [X2,X0,X1] :
( s__instance(X1,X0)
| ~ s__subclass(X2,X0)
| ~ s__instance(X1,X2) ),
inference(forward_subsumption_resolution,[],[f95375,f31784]) ).
fof(f95621,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Object16_2,X0) )
| spl478_163 ),
inference(resolution,[],[f95376,f50345]) ).
fof(f95622,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Object16_3,X0) )
| spl478_165 ),
inference(resolution,[],[f95376,f50353]) ).
fof(f95752,plain,
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| spl478_163 ),
inference(resolution,[],[f95621,f21264]) ).
fof(f95935,plain,
( $false
| spl478_163 ),
inference(forward_subsumption_resolution,[],[f95752,f26911]) ).
fof(f95936,plain,
spl478_163,
inference(avatar_contradiction_clause,[],[f95935]) ).
fof(f95951,plain,
( ~ s__instance(s__Object16_3,s__EngineeringComponent)
| spl478_165 ),
inference(resolution,[],[f95622,f21264]) ).
fof(f96134,plain,
( $false
| spl478_165 ),
inference(forward_subsumption_resolution,[],[f95951,f29215]) ).
fof(f96135,plain,
spl478_165,
inference(avatar_contradiction_clause,[],[f96134]) ).
fof(f96136,plain,
( ~ s__instance(s__Object16_3,s__Object)
| s__overlapsSpatially(s__Object16_2,s__Object16_3)
| ~ s__connected(s__Object16_2,s__Object16_3)
| ~ spl478_163 ),
inference(forward_subsumption_resolution,[],[f91981,f50344]) ).
fof(f96137,plain,
( ~ s__instance(s__Object16_3,s__Object)
| ~ s__connected(s__Object16_2,s__Object16_3)
| ~ spl478_163 ),
inference(forward_subsumption_resolution,[],[f96136,f23520]) ).
fof(f96164,plain,
( ~ s__connected(s__Object16_2,s__Object16_3)
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f96137,f50352]) ).
fof(f96167,plain,
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ spl478_163
| ~ spl478_165 ),
inference(resolution,[],[f96164,f27312]) ).
fof(f96168,plain,
( ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f96167,f26911]) ).
fof(f96170,plain,
( ~ s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f96168,f29215]) ).
fof(f107912,plain,
( ! [X0] :
( ~ s__instance(s__Object16_2,s__EngineeringComponent)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3)
| ~ s__instance(X0,s__EngineeringConnection) )
| ~ spl478_163
| ~ spl478_165 ),
inference(resolution,[],[f26881,f96170]) ).
fof(f107918,plain,
( ! [X0] :
( ~ s__instance(X0,s__EngineeringConnection)
| ~ s__instance(s__Object16_3,s__EngineeringComponent)
| ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3) )
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f107912,f26911]) ).
fof(f107920,plain,
( ! [X0] :
( ~ s__connectsEngineeringComponents(X0,s__Object16_2,s__Object16_3)
| ~ s__instance(X0,s__EngineeringConnection) )
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f107918,f29215]) ).
fof(f107921,plain,
( ~ s__instance(s__Object16_1,s__EngineeringConnection)
| ~ spl478_163
| ~ spl478_165 ),
inference(resolution,[],[f107920,f36054]) ).
fof(f107923,plain,
( $false
| ~ spl478_163
| ~ spl478_165 ),
inference(forward_subsumption_resolution,[],[f107921,f23664]) ).
fof(f107924,plain,
( ~ spl478_163
| ~ spl478_165 ),
inference(avatar_contradiction_clause,[],[f107923]) ).
cnf(s1078,plain,
spl478_163,
inference(sat_conversion,[],[f95936]) ).
cnf(s1079,plain,
spl478_165,
inference(sat_conversion,[],[f96135]) ).
cnf(s1122,plain,
( ~ spl478_163
| ~ spl478_165 ),
inference(sat_conversion,[],[f107924]) ).
cnf(s1123,plain,
~ spl478_163,
inference(rat,[],[s1122,s1079]) ).
cnf(s1124,plain,
$false,
inference(rat,[],[s1078,s1123]) ).
fof(f107925,plain,
$false,
inference(avatar_sat_refutation,[],[s1124]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR089+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n026.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 22:41:42 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 8.00/1.90 % (168067)Will run a generic schedule for satisfiability detection.
% 8.00/1.90 % (168075)dis+10_1_sil=32000:sp=arity:random_seed=3717377436:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 8.00/1.90 % (168073)% WARNING: option uhcvi not known.
% 8.00/1.90 % (168072)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3781888515_2997 on theBenchmark for (2997ds/0Mi)
% 8.00/1.90 % (168073)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=957904824:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 8.00/1.90 % (168074)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1279898624:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 8.00/1.90 % (168076)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3407876411:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 8.00/1.90 % (168077)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4186740939:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 8.00/1.90 % (168078)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4131725913:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 8.00/1.90 % (168075)Instruction limit reached!
% 8.00/1.90 % (168075)------------------------------
% 8.00/1.90 % (168075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.90 % (168075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.90 % (168075)CaDiCaL version: 2.1.3
% 8.00/1.90 % (168075)Termination reason: Instruction limit
% 8.00/1.90 % (168075)Termination phase: Preprocessing 3
% 8.00/1.90 % (168075)Time elapsed: 0.040 s
% 8.00/1.90 % (168075)Peak memory usage: 29 MB
% 8.00/1.90 % (168075)Instructions burned: 105 (million)
% 8.00/1.90 % (168086)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2197514651:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 8.00/1.90 % (168076)Instruction limit reached!
% 8.00/1.90 % (168076)------------------------------
% 8.00/1.90 % (168076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.90 % (168076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.90 % (168076)CaDiCaL version: 2.1.3
% 8.00/1.90 % (168076)Termination reason: Instruction limit
% 8.00/1.90 % (168076)Termination phase: NewCNF
% 8.00/1.90 % (168076)Time elapsed: 0.079 s
% 8.00/1.90 % (168076)Peak memory usage: 31 MB
% 8.00/1.90 % (168076)Instructions burned: 118 (million)
% 8.00/1.90 % (168077)Instruction limit reached!
% 8.00/1.90 % (168077)------------------------------
% 8.00/1.90 % (168077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.90 % (168077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.90 % (168077)CaDiCaL version: 2.1.3
% 8.00/1.90 % (168077)Termination reason: Instruction limit
% 8.00/1.90 % (168077)Termination phase: Clausification
% 8.00/1.90 % (168077)Time elapsed: 0.081 s
% 8.00/1.90 % (168077)Peak memory usage: 30 MB
% 8.00/1.90 % (168077)Instructions burned: 131 (million)
% 8.00/1.90 % (168078)Instruction limit reached!
% 8.00/1.90 % (168078)------------------------------
% 8.00/1.90 % (168078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.90 % (168078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.90 % (168078)CaDiCaL version: 2.1.3
% 8.00/1.90 % (168078)Termination reason: Instruction limit
% 8.00/1.90 % (168078)Termination phase: Property scanning
% 8.00/1.90 % (168078)Time elapsed: 0.099 s
% 8.00/1.90 % (168078)Peak memory usage: 31 MB
% 8.00/1.90 % (168078)Instructions burned: 161 (million)
% 8.00/1.90 % (168088)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3526909512:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 8.00/1.90 % (168089)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=3997939445:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 8.00/1.90 % (168092)ott-21_1_sil=16000:fs=off:random_seed=4255985490:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 8.00/1.90 % (168088)Instruction limit reached!
% 8.00/1.90 % (168088)------------------------------
% 8.00/1.90 % (168088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.00/1.90 % (168088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/1.90 % (168088)CaDiCaL version: 2.1.3
% 8.00/1.90 % (168088)Termination reason: Instruction limit
% 14.70/2.79 % (168088)Termination phase: Clausification
% 14.70/2.79 % (168088)Time elapsed: 0.075 s
% 14.70/2.79 % (168088)Peak memory usage: 30 MB
% 14.70/2.79 % (168088)Instructions burned: 132 (million)
% 14.70/2.79 % (168094)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4265761578:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 14.70/2.79 % (168092)Instruction limit reached!
% 14.70/2.79 % (168092)------------------------------
% 14.70/2.79 % (168092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168092)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168092)Termination reason: Instruction limit
% 14.70/2.79 % (168092)Termination phase: Property scanning
% 14.70/2.79 % (168092)Time elapsed: 0.104 s
% 14.70/2.79 % (168092)Peak memory usage: 31 MB
% 14.70/2.79 % (168092)Instructions burned: 180 (million)
% 14.70/2.79 % (168086)Instruction limit reached!
% 14.70/2.79 % (168086)------------------------------
% 14.70/2.79 % (168086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168086)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168086)Termination reason: Instruction limit
% 14.70/2.79 % (168086)Termination phase: Finite model building preprocessing
% 14.70/2.79 % (168086)Time elapsed: 0.193 s
% 14.70/2.79 % (168086)Peak memory usage: 41 MB
% 14.70/2.79 % (168086)Instructions burned: 718 (million)
% 14.70/2.79 % (168096)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=395877666:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 14.70/2.79 % (168097)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2817591032:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 14.70/2.79 % (168089)Instruction limit reached!
% 14.70/2.79 % (168089)------------------------------
% 14.70/2.79 % (168089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168089)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168089)Termination reason: Instruction limit
% 14.70/2.79 % (168089)Termination phase: Saturation
% 14.70/2.79 % (168089)Time elapsed: 0.331 s
% 14.70/2.79 % (168089)Peak memory usage: 39 MB
% 14.70/2.79 % (168089)Instructions burned: 685 (million)
% 14.70/2.79 % (168094)Instruction limit reached!
% 14.70/2.79 % (168094)------------------------------
% 14.70/2.79 % (168094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168094)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168094)Termination reason: Instruction limit
% 14.70/2.79 % (168094)Termination phase: Saturation
% 14.70/2.79 % (168094)Time elapsed: 0.237 s
% 14.70/2.79 % (168094)Peak memory usage: 35 MB
% 14.70/2.79 % (168094)Instructions burned: 478 (million)
% 14.70/2.79 % (168100)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4077186887:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 14.70/2.79 % (168101)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=3960389896:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 14.70/2.79 % (168097)Instruction limit reached!
% 14.70/2.79 % (168097)------------------------------
% 14.70/2.79 % (168097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168097)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168097)Termination reason: Instruction limit
% 14.70/2.79 % (168097)Termination phase: Saturation
% 14.70/2.79 % (168097)Time elapsed: 0.331 s
% 14.70/2.79 % (168097)Peak memory usage: 44 MB
% 14.70/2.79 % (168097)Instructions burned: 1180 (million)
% 14.70/2.79 % (168104)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1193361014:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 14.70/2.79 % (168096)Instruction limit reached!
% 14.70/2.79 % (168096)------------------------------
% 14.70/2.79 % (168096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.79 % (168096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.79 % (168096)CaDiCaL version: 2.1.3
% 14.70/2.79 % (168096)Termination reason: Instruction limit
% 14.70/2.79 % (168096)Termination phase: Finite model building preprocessing
% 28.54/4.61 % (168096)Time elapsed: 0.414 s
% 28.54/4.61 % (168096)Peak memory usage: 46 MB
% 28.54/4.61 % (168096)Instructions burned: 865 (million)
% 28.54/4.61 % (168106)fmb+10_1_sil=64000:random_seed=2679199285:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 28.54/4.61 % (168101)Instruction limit reached!
% 28.54/4.61 % (168101)------------------------------
% 28.54/4.61 % (168101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168101)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168101)Termination reason: Instruction limit
% 28.54/4.61 % (168101)Termination phase: Saturation
% 28.54/4.61 % (168101)Time elapsed: 0.358 s
% 28.54/4.61 % (168101)Peak memory usage: 42 MB
% 28.54/4.61 % (168101)Instructions burned: 692 (million)
% 28.54/4.61 % (168108)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2944049928:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 28.54/4.61 % (168104)Instruction limit reached!
% 28.54/4.61 % (168104)------------------------------
% 28.54/4.61 % (168104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168104)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168104)Termination reason: Instruction limit
% 28.54/4.61 % (168104)Termination phase: Saturation
% 28.54/4.61 % (168104)Time elapsed: 0.257 s
% 28.54/4.61 % (168104)Peak memory usage: 44 MB
% 28.54/4.61 % (168104)Instructions burned: 880 (million)
% 28.54/4.61 % (168110)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1172808195:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 28.54/4.61 % (168100)Instruction limit reached!
% 28.54/4.61 % (168100)------------------------------
% 28.54/4.61 % (168100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168100)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168100)Termination reason: Instruction limit
% 28.54/4.61 % (168100)Termination phase: Finite model building preprocessing
% 28.54/4.61 % (168100)Time elapsed: 0.428 s
% 28.54/4.61 % (168100)Peak memory usage: 47 MB
% 28.54/4.61 % (168100)Instructions burned: 890 (million)
% 28.54/4.61 % Detected minimum model sizes of [51]
% 28.54/4.61 % Detected maximum model sizes of [max]
% 28.54/4.61 % (168072)Cannot represent all propositional literals internally
% 28.54/4.61 % (168072)Refutation not found, incomplete strategy
% 28.54/4.61 % (168072)------------------------------
% 28.54/4.61 % (168072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168072)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168072)Termination reason: Refutation not found, incomplete strategy
% 28.54/4.61 % (168072)Time elapsed: 0.890 s
% 28.54/4.61 % (168072)Peak memory usage: 59 MB
% 28.54/4.61 % (168072)Instructions burned: 1858 (million)
% 28.54/4.61 % (168112)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2720660915:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 28.54/4.61 % (168072)------------------------------
% 28.54/4.61 % (168072)------------------------------
% 28.54/4.61 % (168114)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3846231061:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 28.54/4.61 % (168110)Instruction limit reached!
% 28.54/4.61 % (168110)------------------------------
% 28.54/4.61 % (168110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168110)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168110)Termination reason: Instruction limit
% 28.54/4.61 % (168110)Termination phase: Finite model building preprocessing
% 28.54/4.61 % (168110)Time elapsed: 0.438 s
% 28.54/4.61 % (168110)Peak memory usage: 46 MB
% 28.54/4.61 % (168110)Instructions burned: 921 (million)
% 28.54/4.61 % (168114)Instruction limit reached!
% 28.54/4.61 % (168114)------------------------------
% 28.54/4.61 % (168114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.54/4.61 % (168114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.54/4.61 % (168114)CaDiCaL version: 2.1.3
% 28.54/4.61 % (168114)Termination reason: Instruction limit
% 28.54/4.61 % (168114)Termination phase: Saturation
% 28.54/4.61 % (168114)Time elapsed: 0.416 s
% 36.27/5.73 % (168114)Peak memory usage: 48 MB
% 36.27/5.73 % (168114)Instructions burned: 1475 (million)
% 36.27/5.73 % (168116)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=491693013:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 36.27/5.73 % Detected minimum model sizes of [51]
% 36.27/5.73 % Detected maximum model sizes of [max]
% 36.27/5.73 % (168106)Cannot represent all propositional literals internally
% 36.27/5.73 % (168106)Refutation not found, incomplete strategy
% 36.27/5.73 % (168106)------------------------------
% 36.27/5.73 % (168106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.27/5.73 % (168106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.27/5.73 % (168106)CaDiCaL version: 2.1.3
% 36.27/5.73 % (168106)Termination reason: Refutation not found, incomplete strategy
% 36.27/5.73 % (168106)Time elapsed: 0.662 s
% 36.27/5.73 % (168106)Peak memory usage: 51 MB
% 36.27/5.73 % (168106)Instructions burned: 1452 (million)
% 36.27/5.73 % (168118)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3138115190:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi)
% 36.27/5.73 % (168106)------------------------------
% 36.27/5.73 % (168106)------------------------------
% 36.27/5.73 % (168120)ott-2_1_sil=16000:newcnf=on:random_seed=3080674720:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 36.27/5.73 % Detected minimum model sizes of [51]
% 36.27/5.73 % Detected maximum model sizes of [max]
% 36.27/5.73 % (168108)Cannot represent all propositional literals internally
% 36.27/5.73 % (168108)Refutation not found, incomplete strategy
% 36.27/5.73 % (168108)------------------------------
% 36.27/5.73 % (168108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.27/5.73 % (168108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.27/5.73 % (168108)CaDiCaL version: 2.1.3
% 36.27/5.73 % (168108)Termination reason: Refutation not found, incomplete strategy
% 36.27/5.73 % (168108)Time elapsed: 0.702 s
% 36.27/5.73 % (168108)Peak memory usage: 52 MB
% 36.27/5.73 % (168108)Instructions burned: 1527 (million)
% 36.27/5.73 % (168108)------------------------------
% 36.27/5.73 % (168108)------------------------------
% 36.27/5.73 % (168122)ott+10_1_sil=32000:tgt=ground:random_seed=3031947441:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi)
% 36.27/5.73 % (168120)Instruction limit reached!
% 36.27/5.73 % (168120)------------------------------
% 36.27/5.73 % (168120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.27/5.73 % (168120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.27/5.73 % (168120)CaDiCaL version: 2.1.3
% 36.27/5.73 % (168120)Termination reason: Instruction limit
% 36.27/5.73 % (168120)Termination phase: Saturation
% 36.27/5.73 % (168120)Time elapsed: 0.439 s
% 36.27/5.73 % (168120)Peak memory usage: 43 MB
% 36.27/5.73 % (168120)Instructions burned: 871 (million)
% 36.27/5.73 % (168124)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2823937233:i=54282_2978 on theBenchmark for (2978ds/54282Mi)
% 36.27/5.73 % (168118)Instruction limit reached!
% 36.27/5.73 % (168118)------------------------------
% 36.27/5.73 % (168118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.27/5.73 % (168118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.27/5.73 % (168118)CaDiCaL version: 2.1.3
% 36.27/5.73 % (168118)Termination reason: Instruction limit
% 36.27/5.73 % (168118)Termination phase: Finite model building preprocessing
% 36.27/5.73 % (168118)Time elapsed: 0.568 s
% 36.27/5.73 % (168118)Peak memory usage: 71 MB
% 36.27/5.73 % (168118)Instructions burned: 2175 (million)
% 36.27/5.73 % (168126)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=625747585:i=3512:aac=none_2977 on theBenchmark for (2977ds/3512Mi)
% 36.27/5.73 % Detected minimum model sizes of [51]
% 36.27/5.73 % Detected maximum model sizes of [max]
% 36.27/5.73 % (168116)Cannot represent all propositional literals internally
% 36.27/5.73 % (168116)Refutation not found, incomplete strategy
% 36.27/5.73 % (168116)------------------------------
% 36.27/5.73 % (168116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.27/5.73 % (168116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.27/5.73 % (168116)CaDiCaL version: 2.1.3
% 36.27/5.73 % (168116)Termination reason: Refutation not found, incomplete strategy
% 36.27/5.73 % (168116)Time elapsed: 0.868 s
% 36.27/5.73 % (168116)Peak memory usage: 58 MB
% 36.27/5.73 % (168116)Instructions burned: 1850 (million)
% 36.27/5.73 % (168116)------------------------------
% 115.15/16.78 % (168116)------------------------------
% 115.15/16.78 % (168128)dis+21_1_sil=32000:sas=cadical:random_seed=431650833:i=3773:amm=off_2974 on theBenchmark for (2974ds/3773Mi)
% 115.15/16.78 % Detected minimum model sizes of [51]
% 115.15/16.78 % Detected maximum model sizes of [max]
% 115.15/16.78 % (168124)Cannot represent all propositional literals internally
% 115.15/16.78 % (168124)Refutation not found, incomplete strategy
% 115.15/16.78 % (168124)------------------------------
% 115.15/16.78 % (168124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.15/16.78 % (168124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/16.78 % (168124)CaDiCaL version: 2.1.3
% 115.15/16.78 % (168124)Termination reason: Refutation not found, incomplete strategy
% 115.15/16.78 % (168124)Time elapsed: 0.888 s
% 115.15/16.78 % (168124)Peak memory usage: 60 MB
% 115.15/16.78 % (168124)Instructions burned: 1871 (million)
% 115.15/16.78 % (168124)------------------------------
% 115.15/16.78 % (168124)------------------------------
% 115.15/16.78 % (168130)ott+11_1_sil=16000:gs=on:random_seed=1019058907:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2969 on theBenchmark for (2969ds/2251Mi)
% 115.15/16.78 % (168126)Instruction limit reached!
% 115.15/16.78 % (168126)------------------------------
% 115.15/16.78 % (168126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.15/16.78 % (168126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/16.78 % (168126)CaDiCaL version: 2.1.3
% 115.15/16.78 % (168126)Termination reason: Instruction limit
% 115.15/16.78 % (168126)Termination phase: Saturation
% 115.15/16.78 % (168126)Time elapsed: 0.891 s
% 115.15/16.78 % (168126)Peak memory usage: 73 MB
% 115.15/16.78 % (168126)Instructions burned: 3514 (million)
% 115.15/16.78 % (168132)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3789564588:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi)
% 115.15/16.78 % Detected minimum model sizes of [51]
% 115.15/16.78 % Detected maximum model sizes of [max]
% 115.15/16.78 % (168132)Cannot represent all propositional literals internally
% 115.15/16.78 % (168132)Refutation not found, incomplete strategy
% 115.15/16.78 % (168132)------------------------------
% 115.15/16.78 % (168132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.15/16.78 % (168132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/16.78 % (168132)CaDiCaL version: 2.1.3
% 115.15/16.78 % (168132)Termination reason: Refutation not found, incomplete strategy
% 115.15/16.78 % (168132)Time elapsed: 0.419 s
% 115.15/16.78 % (168132)Peak memory usage: 53 MB
% 115.15/16.78 % (168132)Instructions burned: 1690 (million)
% 115.15/16.78 % (168132)------------------------------
% 115.15/16.78 % (168132)------------------------------
% 115.15/16.78 % (168134)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2665828058:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2964 on theBenchmark for (2964ds/4591Mi)
% 115.15/16.78 % (168112)Instruction limit reached!
% 115.15/16.78 % (168112)------------------------------
% 115.15/16.78 % (168112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.15/16.78 % (168112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/16.78 % (168112)CaDiCaL version: 2.1.3
% 115.15/16.78 % (168112)Termination reason: Instruction limit
% 115.15/16.78 % (168112)Termination phase: Saturation
% 115.15/16.78 % (168112)Time elapsed: 2.686 s
% 115.15/16.78 % (168112)Peak memory usage: 65 MB
% 115.15/16.78 % (168112)Instructions burned: 5132 (million)
% 115.15/16.78 % (168136)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2000383552:i=29340_2960 on theBenchmark for (2960ds/29340Mi)
% 115.15/16.78 % (168130)Instruction limit reached!
% 115.15/16.78 % (168130)------------------------------
% 115.15/16.78 % (168130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.15/16.78 % (168130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/16.78 % (168130)CaDiCaL version: 2.1.3
% 115.15/16.78 % (168130)Termination reason: Instruction limit
% 115.15/16.78 % (168130)Termination phase: Saturation
% 115.15/16.78 % (168130)Time elapsed: 0.965 s
% 115.15/16.78 % (168130)Peak memory usage: 52 MB
% 115.15/16.78 % (168130)Instructions burned: 2252 (million)
% 115.15/16.78 % (168138)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3811052339:i=5211_2959 on theBenchmark for (2959ds/5211Mi)
% 115.15/16.78 % (168128)Instruction limit reached!
% 115.15/16.78 % (168128)------------------------------
% 115.15/16.78 % (168128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168128)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168128)Termination reason: Instruction limit
% 135.34/19.66 % (168128)Termination phase: Saturation
% 135.34/19.66 % (168128)Time elapsed: 1.786 s
% 135.34/19.66 % (168128)Peak memory usage: 85 MB
% 135.34/19.66 % (168128)Instructions burned: 3775 (million)
% 135.34/19.66 % (168140)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1611680031:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi)
% 135.34/19.66 % (168122)Instruction limit reached!
% 135.34/19.66 % (168122)------------------------------
% 135.34/19.66 % (168122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168122)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168122)Termination reason: Instruction limit
% 135.34/19.66 % (168122)Termination phase: Saturation
% 135.34/19.66 % (168122)Time elapsed: 2.530 s
% 135.34/19.66 % (168122)Peak memory usage: 85 MB
% 135.34/19.66 % (168122)Instructions burned: 5115 (million)
% 135.34/19.66 % (168142)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2355948473:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi)
% 135.34/19.66 % (168134)Instruction limit reached!
% 135.34/19.66 % (168134)------------------------------
% 135.34/19.66 % (168134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168134)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168134)Termination reason: Instruction limit
% 135.34/19.66 % (168134)Termination phase: Saturation
% 135.34/19.66 % (168134)Time elapsed: 1.445 s
% 135.34/19.66 % (168134)Peak memory usage: 97 MB
% 135.34/19.66 % (168134)Instructions burned: 4591 (million)
% 135.34/19.66 % (168144)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=786941041:i=14071_2949 on theBenchmark for (2949ds/14071Mi)
% 135.34/19.66 % Detected minimum model sizes of [51]
% 135.34/19.66 % Detected maximum model sizes of [max]
% 135.34/19.66 % (168140)Cannot represent all propositional literals internally
% 135.34/19.66 % (168140)Refutation not found, incomplete strategy
% 135.34/19.66 % (168140)------------------------------
% 135.34/19.66 % (168140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168140)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168140)Termination reason: Refutation not found, incomplete strategy
% 135.34/19.66 % (168140)Time elapsed: 0.826 s
% 135.34/19.66 % (168140)Peak memory usage: 54 MB
% 135.34/19.66 % (168140)Instructions burned: 1714 (million)
% 135.34/19.66 % Detected minimum model sizes of [51]
% 135.34/19.66 % Detected maximum model sizes of [max]
% 135.34/19.66 % (168142)Cannot represent all propositional literals internally
% 135.34/19.66 % (168142)Refutation not found, incomplete strategy
% 135.34/19.66 % (168142)------------------------------
% 135.34/19.66 % (168142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168142)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168142)Termination reason: Refutation not found, incomplete strategy
% 135.34/19.66 % (168142)Time elapsed: 0.769 s
% 135.34/19.66 % (168142)Peak memory usage: 53 MB
% 135.34/19.66 % (168142)Instructions burned: 1689 (million)
% 135.34/19.66 % (168140)------------------------------
% 135.34/19.66 % (168140)------------------------------
% 135.34/19.66 % (168142)------------------------------
% 135.34/19.66 % (168142)------------------------------
% 135.34/19.66 % (168146)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2290909929:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi)
% 135.34/19.66 % (168147)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1546799362:i=8173:av=off_2947 on theBenchmark for (2947ds/8173Mi)
% 135.34/19.66 % Detected minimum model sizes of [51]
% 135.34/19.66 % Detected maximum model sizes of [max]
% 135.34/19.66 % (168144)Cannot represent all propositional literals internally
% 135.34/19.66 % (168144)Refutation not found, incomplete strategy
% 135.34/19.66 % (168144)------------------------------
% 135.34/19.66 % (168144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.34/19.66 % (168144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.34/19.66 % (168144)CaDiCaL version: 2.1.3
% 135.34/19.66 % (168144)Termination reason: Refutation not found, incomplete strategy
% 151.42/21.90 % (168144)Time elapsed: 0.405 s
% 151.42/21.90 % (168144)Peak memory usage: 53 MB
% 151.42/21.90 % (168144)Instructions burned: 1556 (million)
% 151.42/21.90 % (168144)------------------------------
% 151.42/21.90 % (168144)------------------------------
% 151.42/21.90 % (168150)dis+10_16:1_sil=16000:random_seed=3978182642:i=9155:fsr=off_2945 on theBenchmark for (2945ds/9155Mi)
% 151.42/21.90 % (168138)Instruction limit reached!
% 151.42/21.90 % (168138)------------------------------
% 151.42/21.90 % (168138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168138)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168138)Termination reason: Instruction limit
% 151.42/21.90 % (168138)Termination phase: Saturation
% 151.42/21.90 % (168138)Time elapsed: 2.172 s
% 151.42/21.90 % (168138)Peak memory usage: 66 MB
% 151.42/21.90 % (168138)Instructions burned: 5212 (million)
% 151.42/21.90 % (168152)ott-3_8_sil=64000:random_seed=3486162571:i=20139:bs=on_2937 on theBenchmark for (2937ds/20139Mi)
% 151.42/21.90 % (168150)Instruction limit reached!
% 151.42/21.90 % (168150)------------------------------
% 151.42/21.90 % (168150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168150)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168150)Termination reason: Instruction limit
% 151.42/21.90 % (168150)Termination phase: Saturation
% 151.42/21.90 % (168150)Time elapsed: 2.654 s
% 151.42/21.90 % (168150)Peak memory usage: 157 MB
% 151.42/21.90 % (168150)Instructions burned: 9157 (million)
% 151.42/21.90 % (168154)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=382417:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi)
% 151.42/21.90 % Detected minimum model sizes of [51]
% 151.42/21.90 % Detected maximum model sizes of [max]
% 151.42/21.90 % (168154)Cannot represent all propositional literals internally
% 151.42/21.90 % (168154)Refutation not found, incomplete strategy
% 151.42/21.90 % (168154)------------------------------
% 151.42/21.90 % (168154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168154)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168154)Termination reason: Refutation not found, incomplete strategy
% 151.42/21.90 % (168154)Time elapsed: 0.501 s
% 151.42/21.90 % (168154)Peak memory usage: 58 MB
% 151.42/21.90 % (168154)Instructions burned: 1850 (million)
% 151.42/21.90 % (168154)------------------------------
% 151.42/21.90 % (168154)------------------------------
% 151.42/21.90 % (168156)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=958287004:i=11404_2912 on theBenchmark for (2912ds/11404Mi)
% 151.42/21.90 % (168147)Instruction limit reached!
% 151.42/21.90 % (168147)------------------------------
% 151.42/21.90 % (168147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168147)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168147)Termination reason: Instruction limit
% 151.42/21.90 % (168147)Termination phase: Saturation
% 151.42/21.90 % (168147)Time elapsed: 4.297 s
% 151.42/21.90 % (168147)Peak memory usage: 113 MB
% 151.42/21.90 % (168147)Instructions burned: 8175 (million)
% 151.42/21.90 % (168158)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=73530661:i=14134_2904 on theBenchmark for (2904ds/14134Mi)
% 151.42/21.90 % (168156)Instruction limit reached!
% 151.42/21.90 % (168156)------------------------------
% 151.42/21.90 % (168156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168156)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168156)Termination reason: Instruction limit
% 151.42/21.90 % (168156)Termination phase: Saturation
% 151.42/21.90 % (168156)Time elapsed: 3.980 s
% 151.42/21.90 % (168156)Peak memory usage: 307 MB
% 151.42/21.90 % (168156)Instructions burned: 11406 (million)
% 151.42/21.90 % (168160)dis+33_16_sil=32000:sac=on:random_seed=2524400563:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi)
% 151.42/21.90 % (168160)Instruction limit reached!
% 151.42/21.90 % (168160)------------------------------
% 151.42/21.90 % (168160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.42/21.90 % (168160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.42/21.90 % (168160)CaDiCaL version: 2.1.3
% 151.42/21.90 % (168160)Termination reason: Instruction limit
% 151.42/21.90 % (168160)Termination phase: Saturation
% 151.42/21.90 % (168160)Time elapsed: 3.802 s
% 160.09/23.08 % (168160)Peak memory usage: 97 MB
% 160.09/23.08 % (168160)Instructions burned: 15852 (million)
% 160.09/23.08 % (168162)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=569987250:avsq=on:i=17627:add=on:amm=off_2834 on theBenchmark for (2834ds/17627Mi)
% 160.09/23.08 % (168158)Instruction limit reached!
% 160.09/23.08 % (168158)------------------------------
% 160.09/23.08 % (168158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.09/23.08 % (168158)CaDiCaL version: 2.1.3
% 160.09/23.08 % (168158)Termination reason: Instruction limit
% 160.09/23.08 % (168158)Termination phase: Saturation
% 160.09/23.08 % (168158)Time elapsed: 7.839 s
% 160.09/23.08 % (168158)Peak memory usage: 102 MB
% 160.09/23.08 % (168158)Instructions burned: 14134 (million)
% 160.09/23.08 % (168164)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3906848232:s2a=on:i=53295_2825 on theBenchmark for (2825ds/53295Mi)
% 160.09/23.08 % (168146)Instruction limit reached!
% 160.09/23.08 % (168146)------------------------------
% 160.09/23.08 % (168146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.09/23.08 % (168146)CaDiCaL version: 2.1.3
% 160.09/23.08 % (168146)Termination reason: Instruction limit
% 160.09/23.08 % (168146)Termination phase: Saturation
% 160.09/23.08 % (168146)Time elapsed: 12.572 s
% 160.09/23.08 % (168146)Peak memory usage: 770 MB
% 160.09/23.08 % (168146)Instructions burned: 22566 (million)
% 160.09/23.08 % (168152)Instruction limit reached!
% 160.09/23.08 % (168152)------------------------------
% 160.09/23.08 % (168152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.09/23.08 % (168152)CaDiCaL version: 2.1.3
% 160.09/23.08 % (168152)Termination reason: Instruction limit
% 160.09/23.08 % (168152)Termination phase: Saturation
% 160.09/23.08 % (168152)Time elapsed: 11.568 s
% 160.09/23.08 % (168152)Peak memory usage: 167 MB
% 160.09/23.08 % (168152)Instructions burned: 20140 (million)
% 160.09/23.08 % (168166)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2361390807:i=26857:ins=20_2821 on theBenchmark for (2821ds/26857Mi)
% 160.09/23.08 % (168168)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3225409784:i=28120:bs=on:fsr=off_2820 on theBenchmark for (2820ds/28120Mi)
% 160.09/23.08 % Detected minimum model sizes of [51]
% 160.09/23.08 % Detected maximum model sizes of [max]
% 160.09/23.08 % (168166)Cannot represent all propositional literals internally
% 160.09/23.08 % (168166)Refutation not found, incomplete strategy
% 160.09/23.08 % (168166)------------------------------
% 160.09/23.08 % (168166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.09/23.08 % (168166)CaDiCaL version: 2.1.3
% 160.09/23.08 % (168166)Termination reason: Refutation not found, incomplete strategy
% 160.09/23.08 % (168166)Time elapsed: 0.728 s
% 160.09/23.08 % (168166)Peak memory usage: 53 MB
% 160.09/23.08 % (168166)Instructions burned: 1557 (million)
% 160.09/23.08 % (168166)------------------------------
% 160.09/23.08 % (168166)------------------------------
% 160.09/23.08 % (168170)fmb+10_1_sil=256000:fmbss=7:random_seed=1566864961:fmbsr=1.6:i=182295_2813 on theBenchmark for (2813ds/182295Mi)
% 160.09/23.08 % (168136)Instruction limit reached!
% 160.09/23.08 % (168136)------------------------------
% 160.09/23.08 % (168136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.09/23.08 % (168136)CaDiCaL version: 2.1.3
% 160.09/23.08 % (168136)Termination reason: Instruction limit
% 160.09/23.08 % (168136)Termination phase: Saturation
% 160.09/23.08 % (168136)Time elapsed: 14.999 s
% 160.09/23.08 % (168136)Peak memory usage: 75 MB
% 160.09/23.08 % (168136)Instructions burned: 29342 (million)
% 160.09/23.08 % (168172)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3066315350:i=44625:gsp=on_2810 on theBenchmark for (2810ds/44625Mi)
% 160.09/23.08 % Detected minimum model sizes of [51]
% 160.09/23.08 % Detected maximum model sizes of [max]
% 160.09/23.08 % (168170)Cannot represent all propositional literals internally
% 160.09/23.08 % (168170)Refutation not found, incomplete strategy
% 160.09/23.08 % (168170)------------------------------
% 160.09/23.08 % (168170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 160.09/23.08 % (168170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.02/25.18 % (168170)CaDiCaL version: 2.1.3
% 175.02/25.18 % (168170)Termination reason: Refutation not found, incomplete strategy
% 175.02/25.18 % (168170)Time elapsed: 0.728 s
% 175.02/25.18 % (168170)Peak memory usage: 53 MB
% 175.02/25.18 % (168170)Instructions burned: 1556 (million)
% 175.02/25.18 % (168170)------------------------------
% 175.02/25.18 % (168170)------------------------------
% 175.02/25.18 % (168174)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1521657814:i=160505_2805 on theBenchmark for (2805ds/160505Mi)
% 175.02/25.18 % Detected minimum model sizes of [51]
% 175.02/25.18 % Detected maximum model sizes of [max]
% 175.02/25.18 % (168172)Cannot represent all propositional literals internally
% 175.02/25.18 % (168172)Refutation not found, incomplete strategy
% 175.02/25.18 % (168172)------------------------------
% 175.02/25.18 % (168172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.02/25.18 % (168172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.02/25.18 % (168172)CaDiCaL version: 2.1.3
% 175.02/25.18 % (168172)Termination reason: Refutation not found, incomplete strategy
% 175.02/25.18 % (168172)Time elapsed: 0.792 s
% 175.02/25.18 % (168172)Peak memory usage: 56 MB
% 175.02/25.18 % (168172)Instructions burned: 1671 (million)
% 175.02/25.18 % (168172)------------------------------
% 175.02/25.18 % (168172)------------------------------
% 175.02/25.18 % (168176)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=840000247:fmbsr=1.3:i=225729_2802 on theBenchmark for (2802ds/225729Mi)
% 175.02/25.18 % Detected minimum model sizes of [51]
% 175.02/25.18 % Detected maximum model sizes of [max]
% 175.02/25.18 % (168174)Cannot represent all propositional literals internally
% 175.02/25.18 % (168174)Refutation not found, incomplete strategy
% 175.02/25.18 % (168174)------------------------------
% 175.02/25.18 % (168174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.02/25.18 % (168174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.02/25.18 % (168174)CaDiCaL version: 2.1.3
% 175.02/25.18 % (168174)Termination reason: Refutation not found, incomplete strategy
% 175.02/25.18 % (168174)Time elapsed: 0.737 s
% 175.02/25.18 % (168174)Peak memory usage: 53 MB
% 175.02/25.18 % (168174)Instructions burned: 1556 (million)
% 175.02/25.18 % (168174)------------------------------
% 175.02/25.18 % (168174)------------------------------
% 175.02/25.18 % (168178)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=949994480:fmbsr=2:i=185024:ins=7_2797 on theBenchmark for (2797ds/185024Mi)
% 175.02/25.18 % Detected minimum model sizes of [51]
% 175.02/25.18 % Detected maximum model sizes of [max]
% 175.02/25.18 % (168176)Cannot represent all propositional literals internally
% 175.02/25.18 % (168176)Refutation not found, incomplete strategy
% 175.02/25.18 % (168176)------------------------------
% 175.02/25.18 % (168176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.02/25.18 % (168176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.02/25.18 % (168176)CaDiCaL version: 2.1.3
% 175.02/25.18 % (168176)Termination reason: Refutation not found, incomplete strategy
% 175.02/25.18 % (168176)Time elapsed: 0.731 s
% 175.02/25.18 % (168176)Peak memory usage: 54 MB
% 175.02/25.18 % (168176)Instructions burned: 1556 (million)
% 175.02/25.18 % (168176)------------------------------
% 175.02/25.18 % (168176)------------------------------
% 175.02/25.18 % (168180)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2872187487:rtra=on_2794 on theBenchmark for (2794ds/0Mi)
% 175.02/25.18 % Detected minimum model sizes of [51]
% 175.02/25.18 % Detected maximum model sizes of [max]
% 175.02/25.18 % (168178)Cannot represent all propositional literals internally
% 175.02/25.18 % (168178)Refutation not found, incomplete strategy
% 175.02/25.18 % (168178)------------------------------
% 175.02/25.18 % (168178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.02/25.18 % (168178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.02/25.18 % (168178)CaDiCaL version: 2.1.3
% 175.02/25.18 % (168178)Termination reason: Refutation not found, incomplete strategy
% 175.02/25.18 % (168178)Time elapsed: 0.732 s
% 175.02/25.18 % (168178)Peak memory usage: 53 MB
% 175.02/25.18 % (168178)Instructions burned: 1557 (million)
% 175.02/25.18 % (168178)------------------------------
% 175.02/25.18 % (168178)------------------------------
% 175.02/25.18 % (168182)% WARNING: option uhcvi not known.
% 175.02/25.18 % (168182)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1246289268:i=271062:add=off:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/271062Mi)
% 175.02/25.18 % Detected minimum model sizes of [51]
% 175.02/25.18 % Detected maximum model sizes of [max]
% 200.56/28.82 % (168180)Cannot represent all propositional literals internally
% 200.56/28.82 % (168180)Refutation not found, incomplete strategy
% 200.56/28.82 % (168180)------------------------------
% 200.56/28.82 % (168180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168180)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168180)Termination reason: Refutation not found, incomplete strategy
% 200.56/28.82 % (168180)Time elapsed: 1.059 s
% 200.56/28.82 % (168180)Peak memory usage: 63 MB
% 200.56/28.82 % (168180)Instructions burned: 1890 (million)
% 200.56/28.82 % (168180)------------------------------
% 200.56/28.82 % (168180)------------------------------
% 200.56/28.82 % (168184)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3687269528:i=176048:add=on:rtra=on:rawr=on_2783 on theBenchmark for (2783ds/176048Mi)
% 200.56/28.82 % (168162)Instruction limit reached!
% 200.56/28.82 % (168162)------------------------------
% 200.56/28.82 % (168162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168162)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168162)Termination reason: Instruction limit
% 200.56/28.82 % (168162)Termination phase: Saturation
% 200.56/28.82 % (168162)Time elapsed: 5.705 s
% 200.56/28.82 % (168162)Peak memory usage: 370 MB
% 200.56/28.82 % (168162)Instructions burned: 17630 (million)
% 200.56/28.82 % (168186)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3037442535:i=206:fgj=on:rtra=on_2777 on theBenchmark for (2777ds/206Mi)
% 200.56/28.82 % (168186)Instruction limit reached!
% 200.56/28.82 % (168186)------------------------------
% 200.56/28.82 % (168186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168186)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168186)Termination reason: Instruction limit
% 200.56/28.82 % (168186)Termination phase: Property scanning
% 200.56/28.82 % (168186)Time elapsed: 0.101 s
% 200.56/28.82 % (168186)Peak memory usage: 34 MB
% 200.56/28.82 % (168186)Instructions burned: 206 (million)
% 200.56/28.82 % (168188)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=897039598:i=232:rtra=on_2775 on theBenchmark for (2775ds/232Mi)
% 200.56/28.82 % (168188)Instruction limit reached!
% 200.56/28.82 % (168188)------------------------------
% 200.56/28.82 % (168188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168188)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168188)Termination reason: Instruction limit
% 200.56/28.82 % (168188)Termination phase: Property scanning
% 200.56/28.82 % (168188)Time elapsed: 0.112 s
% 200.56/28.82 % (168188)Peak memory usage: 36 MB
% 200.56/28.82 % (168188)Instructions burned: 234 (million)
% 200.56/28.82 % (168190)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3441814929:i=262:rtra=on_2774 on theBenchmark for (2774ds/262Mi)
% 200.56/28.82 % (168190)Instruction limit reached!
% 200.56/28.82 % (168190)------------------------------
% 200.56/28.82 % (168190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168190)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168190)Termination reason: Instruction limit
% 200.56/28.82 % (168190)Termination phase: Saturation
% 200.56/28.82 % (168190)Time elapsed: 0.114 s
% 200.56/28.82 % (168190)Peak memory usage: 35 MB
% 200.56/28.82 % (168190)Instructions burned: 267 (million)
% 200.56/28.82 % (168192)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1971528140:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2773 on theBenchmark for (2773ds/318Mi)
% 200.56/28.82 % (168192)Instruction limit reached!
% 200.56/28.82 % (168192)------------------------------
% 200.56/28.82 % (168192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 200.56/28.82 % (168192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.56/28.82 % (168192)CaDiCaL version: 2.1.3
% 200.56/28.82 % (168192)Termination reason: Instruction limit
% 200.56/28.82 % (168192)Termination phase: Property scanning
% 200.56/28.82 % (168192)Time elapsed: 0.138 s
% 200.56/28.82 % (168192)Peak memory usage: 38 MB
% 200.56/28.82 % (168192)Instructions burned: 319 (million)
% 200.56/28.82 % (168194)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=792046365:i=1428:nm=2:rtra=on_2771 on theBenchmark for (2771ds/1428Mi)
% 169.55/32.90 % (168194)Instruction limit reached!
% 169.55/32.90 % (168194)------------------------------
% 169.55/32.90 % (168194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/32.90 % (168194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/32.90 % (168194)CaDiCaL version: 2.1.3
% 169.55/32.90 % (168194)Termination reason: Instruction limit
% 169.55/32.90 % (168194)Termination phase: Finite model building preprocessing
% 169.55/32.90 % (168194)Time elapsed: 0.445 s
% 169.55/32.90 % (168194)Peak memory usage: 53 MB
% 169.55/32.90 % (168194)Instructions burned: 1433 (million)
% 169.55/32.90 % (168196)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3824134927:i=262:bd=preordered:rtra=on:fsd=on_2767 on theBenchmark for (2767ds/262Mi)
% 169.55/32.90 % (168196)Instruction limit reached!
% 169.55/32.90 % (168196)------------------------------
% 169.55/32.90 % (168196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/32.90 % (168196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/32.90 % (168196)CaDiCaL version: 2.1.3
% 169.55/32.90 % (168196)Termination reason: Instruction limit
% 169.55/32.90 % (168196)Termination phase: Property scanning
% 169.55/32.90 % (168196)Time elapsed: 0.114 s
% 169.55/32.90 % (168196)Peak memory usage: 35 MB
% 169.55/32.90 % (168196)Instructions burned: 263 (million)
% 169.55/32.90 % (168198)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1898640963:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2765 on theBenchmark for (2765ds/1368Mi)
% 169.55/32.90 % (168198)Instruction limit reached!
% 169.55/32.90 % (168198)------------------------------
% 169.55/32.90 % (168198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.55/32.90 % (168198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.55/32.90 % (168198)CaDiCaL version: 2.1.3
% 169.55/32.90 % (168198)Termination reason: Instruction limit
% 169.55/32.90 % (168198)Termination phase: Saturation
% 169.55/32.90 % (168198)Time elapsed: 0.502 s
% 169.55/32.90 % (168198)Peak memory usage: 50 MB
% 169.55/32.90 % (168198)Instructions burned: 1370 (million)
% 228.45/32.90 % (168200)ott-21_1_sil=16000:si=on:fs=off:random_seed=1398838005:i=360:av=off:fsr=off:rtra=on_2760 on theBenchmark for (2760ds/360Mi)
% 228.45/32.90 % (168200)Instruction limit reached!
% 228.45/32.90 % (168200)------------------------------
% 228.45/32.90 % (168200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168200)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168200)Termination reason: Instruction limit
% 228.45/32.90 % (168200)Termination phase: Saturation
% 228.45/32.90 % (168200)Time elapsed: 0.140 s
% 228.45/32.90 % (168200)Peak memory usage: 36 MB
% 228.45/32.90 % (168200)Instructions burned: 364 (million)
% 228.45/32.90 % (168202)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3626143381:i=954:bd=all:rtra=on_2759 on theBenchmark for (2759ds/954Mi)
% 228.45/32.90 % (168202)Instruction limit reached!
% 228.45/32.90 % (168202)------------------------------
% 228.45/32.90 % (168202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168202)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168202)Termination reason: Instruction limit
% 228.45/32.90 % (168202)Termination phase: Saturation
% 228.45/32.90 % (168202)Time elapsed: 0.351 s
% 228.45/32.90 % (168202)Peak memory usage: 45 MB
% 228.45/32.90 % (168202)Instructions burned: 954 (million)
% 228.45/32.90 % (168204)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1012892085:fmbsr=1.3:i=1730:ins=25:rtra=on_2755 on theBenchmark for (2755ds/1730Mi)
% 228.45/32.90 % Detected minimum model sizes of [51]
% 228.45/32.90 % Detected maximum model sizes of [max]
% 228.45/32.90 % (168204)Cannot represent all propositional literals internally
% 228.45/32.90 % (168204)Refutation not found, incomplete strategy
% 228.45/32.90 % (168204)------------------------------
% 228.45/32.90 % (168204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168204)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168204)Termination reason: Refutation not found, incomplete strategy
% 228.45/32.90 % (168204)Time elapsed: 0.465 s
% 228.45/32.90 % (168204)Peak memory usage: 57 MB
% 228.45/32.90 % (168204)Instructions burned: 1522 (million)
% 228.45/32.90 % (168204)------------------------------
% 228.45/32.90 % (168204)------------------------------
% 228.45/32.90 % (168206)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3979060927:i=2358:rtra=on_2750 on theBenchmark for (2750ds/2358Mi)
% 228.45/32.90 % (168206)Instruction limit reached!
% 228.45/32.90 % (168206)------------------------------
% 228.45/32.90 % (168206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168206)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168206)Termination reason: Instruction limit
% 228.45/32.90 % (168206)Termination phase: Saturation
% 228.45/32.90 % (168206)Time elapsed: 0.821 s
% 228.45/32.90 % (168206)Peak memory usage: 55 MB
% 228.45/32.90 % (168206)Instructions burned: 2361 (million)
% 228.45/32.90 % (168208)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=933633720:i=1778:ins=1:rtra=on_2742 on theBenchmark for (2742ds/1778Mi)
% 228.45/32.90 % (168208)Cannot represent all propositional literals internally
% 228.45/32.90 % (168208)Refutation not found, incomplete strategy
% 228.45/32.90 % (168208)------------------------------
% 228.45/32.90 % (168208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168208)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168208)Termination reason: Refutation not found, incomplete strategy
% 228.45/32.90 % (168208)Time elapsed: 0.503 s
% 228.45/32.90 % (168208)Peak memory usage: 58 MB
% 228.45/32.90 % (168208)Instructions burned: 1602 (million)
% 228.45/32.90 % (168208)------------------------------
% 228.45/32.90 % (168208)------------------------------
% 228.45/32.90 % (168210)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3015442623:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2736 on theBenchmark for (2736ds/1384Mi)
% 228.45/32.90 % (168210)Instruction limit reached!
% 228.45/32.90 % (168210)------------------------------
% 228.45/32.90 % (168210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168210)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168210)Termination reason: Instruction limit
% 228.45/32.90 % (168210)Termination phase: Saturation
% 228.45/32.90 % (168210)Time elapsed: 0.579 s
% 228.45/32.90 % (168210)Peak memory usage: 55 MB
% 228.45/32.90 % (168210)Instructions burned: 1385 (million)
% 228.45/32.90 % (168212)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=569820734:i=1758:kws=inv_precedence:fsr=off:rtra=on_2730 on theBenchmark for (2730ds/1758Mi)
% 228.45/32.90 % (168212)Instruction limit reached!
% 228.45/32.90 % (168212)------------------------------
% 228.45/32.90 % (168212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168212)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168212)Termination reason: Instruction limit
% 228.45/32.90 % (168212)Termination phase: Saturation
% 228.45/32.90 % (168212)Time elapsed: 0.613 s
% 228.45/32.90 % (168212)Peak memory usage: 61 MB
% 228.45/32.90 % (168212)Instructions burned: 1760 (million)
% 228.45/32.90 % (168214)fmb+10_1_sil=64000:si=on:random_seed=1955751331:i=44122:nm=2:rtra=on:gsp=on_2724 on theBenchmark for (2724ds/44122Mi)
% 228.45/32.90 % Detected minimum model sizes of [51]
% 228.45/32.90 % Detected maximum model sizes of [max]
% 228.45/32.90 % (168214)Cannot represent all propositional literals internally
% 228.45/32.90 % (168214)Refutation not found, incomplete strategy
% 228.45/32.90 % (168214)------------------------------
% 228.45/32.90 % (168214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168214)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168214)Termination reason: Refutation not found, incomplete strategy
% 228.45/32.90 % (168214)Time elapsed: 0.468 s
% 228.45/32.90 % (168214)Peak memory usage: 55 MB
% 228.45/32.90 % (168214)Instructions burned: 1489 (million)
% 228.45/32.90 % (168214)------------------------------
% 228.45/32.90 % (168214)------------------------------
% 228.45/32.90 % (168216)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3635297605:i=19030:nm=5:rtra=on_2719 on theBenchmark for (2719ds/19030Mi)
% 228.45/32.90 % Detected minimum model sizes of [51]
% 228.45/32.90 % Detected maximum model sizes of [max]
% 228.45/32.90 % (168216)Cannot represent all propositional literals internally
% 228.45/32.90 % (168216)Refutation not found, incomplete strategy
% 228.45/32.90 % (168216)------------------------------
% 228.45/32.90 % (168216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168216)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168216)Termination reason: Refutation not found, incomplete strategy
% 228.45/32.90 % (168216)Time elapsed: 0.491 s
% 228.45/32.90 % (168216)Peak memory usage: 56 MB
% 228.45/32.90 % (168216)Instructions burned: 1566 (million)
% 228.45/32.90 % (168216)------------------------------
% 228.45/32.90 % (168216)------------------------------
% 228.45/32.90 % (168218)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=715241233:fmbsr=1.7:i=1840:rtra=on_2714 on theBenchmark for (2714ds/1840Mi)
% 228.45/32.90 % Detected minimum model sizes of [51]
% 228.45/32.90 % Detected maximum model sizes of [max]
% 228.45/32.90 % (168218)Cannot represent all propositional literals internally
% 228.45/32.90 % (168218)Refutation not found, incomplete strategy
% 228.45/32.90 % (168218)------------------------------
% 228.45/32.90 % (168218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.90 % (168218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.90 % (168218)CaDiCaL version: 2.1.3
% 228.45/32.90 % (168218)Termination reason: Refutation not found, incomplete strategy
% 228.45/32.90 % (168218)Time elapsed: 0.501 s
% 228.45/32.90 % (168218)Peak memory usage: 57 MB
% 228.45/32.90 % (168218)Instructions burned: 1596 (million)
% 228.45/32.90 % (168218)------------------------------
% 228.45/32.90 % (168218)------------------------------
% 228.45/32.90 % (168220)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2381501244:i=10262:rtra=on_2708 on theBenchmark for (2708ds/10262Mi)
% 228.45/32.90 % (168220) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-168067-168220"...
% 228.45/32.90 % (168220)...printing done.
% 228.45/32.90 % (168220)Refutation found. Thanks to Tanya!
% 228.45/32.90 % SZS status Theorem for theBenchmark
% 228.45/32.90 % SZS output start Proof for theBenchmark
% See solution above
% 228.45/32.91 % (168220)------------------------------
% 228.45/32.91 % (168220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 228.45/32.91 % (168220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.45/32.91 % (168220)CaDiCaL version: 2.1.3
% 228.45/32.91 % (168220)Termination reason: Refutation
% 228.45/32.91 % (168220)Time elapsed: 3.149 s
% 228.45/32.91 % (168220)Peak memory usage: 71 MB
% 228.45/32.91 % (168220)Instructions burned: 8812 (million)
% 228.45/32.91 % (168067)Success in time 32.645 s
% 228.45/32.91 % Vampire exiting
%------------------------------------------------------------------------------