%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR082+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:03 AM UTC 2026
% Result : Theorem 143.23s 24.36s
% Output : Refutation 143.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 19
% Syntax : Number of formulae : 105 ( 25 unt; 8 def)
% Number of atoms : 259 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 294 ( 140 ~; 133 |; 6 &)
% ( 8 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 9 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 55 ( 0 sgn 51 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_27) ).
fof(f826,axiom,
s__subclass(s__Agent,s__Object),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_827) ).
fof(f829,axiom,
s__subclass(s__SentientAgent,s__Agent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_830) ).
fof(f831,axiom,
s__subclass(s__CognitiveAgent,s__SentientAgent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_832) ).
fof(f6472,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__CognitiveAgent)
=> s__capability(s__Reasoning,s__agent__m,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_6509) ).
fof(f6823,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__SentientAgent)
=> s__capability(s__Perception,s__experiencer__m,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_6882) ).
fof(f7056,axiom,
s__subclass(s__Organism,s__Agent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7129) ).
fof(f7207,axiom,
s__subclass(s__Human,s__CognitiveAgent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7281) ).
fof(f16749,axiom,
s__instance(s__Jane8_1,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f16750,conjecture,
? [X0,X1] :
( s__capability(s__Reasoning,X0,s__Jane8_1)
& s__capability(s__Perception,X1,s__Jane8_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f16751,negated_conjecture,
~ ? [X0,X1] :
( s__capability(s__Reasoning,X0,s__Jane8_1)
& s__capability(s__Perception,X1,s__Jane8_1) ),
inference(negated_conjecture,[status(cth)],[f16750]) ).
fof(f17018,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f17019,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f17020,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f17019]) ).
fof(f23877,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f6472]) ).
fof(f23878,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f23877]) ).
fof(f24003,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f6823]) ).
fof(f24004,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f24003]) ).
fof(f27119,plain,
! [X0,X1] :
( ~ s__capability(s__Reasoning,X0,s__Jane8_1)
| ~ s__capability(s__Perception,X1,s__Jane8_1) ),
inference(ennf_transformation,[],[f16751]) ).
fof(f28679,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17018]) ).
fof(f28680,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17018]) ).
fof(f28681,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17020]) ).
fof(f29537,plain,
s__subclass(s__Agent,s__Object),
inference(cnf_transformation,[],[f826]) ).
fof(f29542,plain,
s__subclass(s__SentientAgent,s__Agent),
inference(cnf_transformation,[],[f829]) ).
fof(f29544,plain,
s__subclass(s__CognitiveAgent,s__SentientAgent),
inference(cnf_transformation,[],[f831]) ).
fof(f35769,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f23878]) ).
fof(f36262,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f24004]) ).
fof(f36538,plain,
s__subclass(s__Organism,s__Agent),
inference(cnf_transformation,[],[f7056]) ).
fof(f36700,plain,
s__subclass(s__Human,s__CognitiveAgent),
inference(cnf_transformation,[],[f7207]) ).
fof(f48576,plain,
s__instance(s__Jane8_1,s__Human),
inference(cnf_transformation,[],[f16749]) ).
fof(f48577,plain,
! [X0,X1] :
( ~ s__capability(s__Reasoning,X0,s__Jane8_1)
| ~ s__capability(s__Perception,X1,s__Jane8_1) ),
inference(cnf_transformation,[],[f27119]) ).
fof(f49150,definition,
( spl1514_1
<=> ! [X1] : ~ s__capability(s__Perception,X1,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[spl1514_1])],[avatar_definition]) ).
fof(f49151,plain,
( ! [X1] : ~ s__capability(s__Perception,X1,s__Jane8_1)
| ~ spl1514_1 ),
inference(avatar_component_clause,[],[f49150]) ).
fof(f49153,definition,
( spl1514_2
<=> ! [X0] : ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[spl1514_2])],[avatar_definition]) ).
fof(f49154,plain,
( ! [X0] : ~ s__capability(s__Reasoning,X0,s__Jane8_1)
| ~ spl1514_2 ),
inference(avatar_component_clause,[],[f49153]) ).
fof(f49155,plain,
( spl1514_1
| spl1514_2 ),
inference(avatar_split_clause,[],[f48577,f49153,f49150]) ).
fof(f56254,plain,
( ~ s__instance(s__Jane8_1,s__CognitiveAgent)
| ~ s__instance(s__Jane8_1,s__Object)
| ~ spl1514_2 ),
inference(resolution,[],[f35769,f49154]) ).
fof(f56256,definition,
( spl1514_279
<=> s__instance(s__Jane8_1,s__Object) ),
introduced(definition,[new_symbols(definition,[spl1514_279])],[avatar_definition]) ).
fof(f56258,plain,
( ~ s__instance(s__Jane8_1,s__Object)
| spl1514_279 ),
inference(avatar_component_clause,[],[f56256]) ).
fof(f56260,definition,
( spl1514_280
<=> s__instance(s__Jane8_1,s__CognitiveAgent) ),
introduced(definition,[new_symbols(definition,[spl1514_280])],[avatar_definition]) ).
fof(f56261,plain,
( s__instance(s__Jane8_1,s__CognitiveAgent)
| ~ spl1514_280 ),
inference(avatar_component_clause,[],[f56260]) ).
fof(f56262,plain,
( ~ s__instance(s__Jane8_1,s__CognitiveAgent)
| spl1514_280 ),
inference(avatar_component_clause,[],[f56260]) ).
fof(f56263,plain,
( ~ spl1514_279
| ~ spl1514_280
| ~ spl1514_2 ),
inference(avatar_split_clause,[],[f56254,f49153,f56260,f56256]) ).
fof(f56653,plain,
( ~ s__instance(s__Jane8_1,s__SentientAgent)
| ~ s__instance(s__Jane8_1,s__Object)
| ~ spl1514_1 ),
inference(resolution,[],[f36262,f49151]) ).
fof(f56655,definition,
( spl1514_311
<=> s__instance(s__Jane8_1,s__SentientAgent) ),
introduced(definition,[new_symbols(definition,[spl1514_311])],[avatar_definition]) ).
fof(f56656,plain,
( s__instance(s__Jane8_1,s__SentientAgent)
| ~ spl1514_311 ),
inference(avatar_component_clause,[],[f56655]) ).
fof(f56657,plain,
( ~ s__instance(s__Jane8_1,s__SentientAgent)
| spl1514_311 ),
inference(avatar_component_clause,[],[f56655]) ).
fof(f56658,plain,
( ~ spl1514_279
| ~ spl1514_311
| ~ spl1514_1 ),
inference(avatar_split_clause,[],[f56653,f49150,f56655,f56256]) ).
fof(f70977,definition,
( spl1514_362
<=> s__instance(s__Object,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl1514_362])],[avatar_definition]) ).
fof(f70978,plain,
( s__instance(s__Object,s__SetOrClass)
| ~ spl1514_362 ),
inference(avatar_component_clause,[],[f70977]) ).
fof(f70979,plain,
( ~ s__instance(s__Object,s__SetOrClass)
| spl1514_362 ),
inference(avatar_component_clause,[],[f70977]) ).
fof(f71147,definition,
( spl1514_380
<=> s__instance(s__CognitiveAgent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl1514_380])],[avatar_definition]) ).
fof(f71148,plain,
( s__instance(s__CognitiveAgent,s__SetOrClass)
| ~ spl1514_380 ),
inference(avatar_component_clause,[],[f71147]) ).
fof(f71149,plain,
( ~ s__instance(s__CognitiveAgent,s__SetOrClass)
| spl1514_380 ),
inference(avatar_component_clause,[],[f71147]) ).
fof(f71438,definition,
( spl1514_408
<=> s__instance(s__Agent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl1514_408])],[avatar_definition]) ).
fof(f71439,plain,
( s__instance(s__Agent,s__SetOrClass)
| ~ spl1514_408 ),
inference(avatar_component_clause,[],[f71438]) ).
fof(f71440,plain,
( ~ s__instance(s__Agent,s__SetOrClass)
| spl1514_408 ),
inference(avatar_component_clause,[],[f71438]) ).
fof(f71469,plain,
( ! [X0] : ~ s__subclass(X0,s__Agent)
| spl1514_408 ),
inference(resolution,[],[f71440,f28679]) ).
fof(f71478,plain,
( $false
| spl1514_408 ),
inference(resolution,[],[f71469,f36538]) ).
fof(f71491,plain,
spl1514_408,
inference(avatar_contradiction_clause,[],[f71478]) ).
fof(f71514,plain,
( ! [X0] : ~ s__subclass(X0,s__CognitiveAgent)
| spl1514_380 ),
inference(resolution,[],[f71149,f28679]) ).
fof(f71522,plain,
( $false
| spl1514_380 ),
inference(resolution,[],[f71514,f36700]) ).
fof(f71523,plain,
spl1514_380,
inference(avatar_contradiction_clause,[],[f71522]) ).
fof(f71548,plain,
( ! [X0] : ~ s__subclass(X0,s__Object)
| spl1514_362 ),
inference(resolution,[],[f70979,f28679]) ).
fof(f71556,plain,
( $false
| spl1514_362 ),
inference(resolution,[],[f71548,f29537]) ).
fof(f71575,plain,
spl1514_362,
inference(avatar_contradiction_clause,[],[f71556]) ).
fof(f266784,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(s__Object,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_279 ),
inference(resolution,[],[f28681,f56258]) ).
fof(f267016,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_279
| ~ spl1514_362 ),
inference(forward_subsumption_resolution,[],[f266784,f70978]) ).
fof(f267770,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Jane8_1,X0) )
| spl1514_279
| ~ spl1514_362 ),
inference(forward_subsumption_resolution,[],[f267016,f28680]) ).
fof(f268526,plain,
( ~ s__instance(s__Jane8_1,s__Agent)
| spl1514_279
| ~ spl1514_362 ),
inference(resolution,[],[f267770,f29537]) ).
fof(f268537,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(s__Agent,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_279
| ~ spl1514_362 ),
inference(resolution,[],[f268526,f28681]) ).
fof(f268538,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_279
| ~ spl1514_362
| ~ spl1514_408 ),
inference(forward_subsumption_resolution,[],[f268537,f71439]) ).
fof(f268539,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Agent)
| ~ s__instance(s__Jane8_1,X0) )
| spl1514_279
| ~ spl1514_362
| ~ spl1514_408 ),
inference(forward_subsumption_resolution,[],[f268538,f28680]) ).
fof(f274808,plain,
( ~ s__instance(s__Jane8_1,s__SentientAgent)
| spl1514_279
| ~ spl1514_362
| ~ spl1514_408 ),
inference(resolution,[],[f268539,f29542]) ).
fof(f274825,plain,
( ! [X0] :
( ~ s__subclass(X0,s__CognitiveAgent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(s__CognitiveAgent,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_280 ),
inference(resolution,[],[f56262,f28681]) ).
fof(f274826,plain,
( ! [X0] :
( ~ s__subclass(X0,s__CognitiveAgent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_280
| ~ spl1514_380 ),
inference(forward_subsumption_resolution,[],[f274825,f71148]) ).
fof(f274828,plain,
( ! [X0] :
( ~ s__subclass(X0,s__CognitiveAgent)
| ~ s__instance(s__Jane8_1,X0) )
| spl1514_280
| ~ spl1514_380 ),
inference(forward_subsumption_resolution,[],[f274826,f28680]) ).
fof(f274841,plain,
( ~ s__instance(s__Jane8_1,s__Human)
| spl1514_280
| ~ spl1514_380 ),
inference(resolution,[],[f274828,f36700]) ).
fof(f274842,plain,
( $false
| spl1514_280
| ~ spl1514_380 ),
inference(forward_subsumption_resolution,[],[f274841,f48576]) ).
fof(f274843,plain,
( spl1514_280
| ~ spl1514_380 ),
inference(avatar_contradiction_clause,[],[f274842]) ).
fof(f274855,plain,
( ! [X0] :
( ~ s__subclass(X0,s__SentientAgent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(s__SentientAgent,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_311 ),
inference(resolution,[],[f56657,f28681]) ).
fof(f274856,plain,
( ! [X0] :
( ~ s__subclass(X0,s__SentientAgent)
| ~ s__instance(s__Jane8_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_311 ),
inference(forward_subsumption_resolution,[],[f274855,f28679]) ).
fof(f274857,plain,
( ! [X0] :
( ~ s__subclass(X0,s__SentientAgent)
| ~ s__instance(s__Jane8_1,X0) )
| spl1514_311 ),
inference(forward_subsumption_resolution,[],[f274856,f28680]) ).
fof(f275023,plain,
( ~ s__instance(s__Jane8_1,s__CognitiveAgent)
| spl1514_311 ),
inference(resolution,[],[f274857,f29544]) ).
fof(f275024,plain,
( $false
| ~ spl1514_280
| spl1514_311 ),
inference(forward_subsumption_resolution,[],[f275023,f56261]) ).
fof(f275025,plain,
( ~ spl1514_280
| spl1514_311 ),
inference(avatar_contradiction_clause,[],[f275024]) ).
fof(f275027,plain,
( $false
| spl1514_279
| ~ spl1514_311
| ~ spl1514_362
| ~ spl1514_408 ),
inference(forward_subsumption_resolution,[],[f56656,f274808]) ).
fof(f275028,plain,
( spl1514_279
| ~ spl1514_311
| ~ spl1514_362
| ~ spl1514_408 ),
inference(avatar_contradiction_clause,[],[f275027]) ).
cnf(s1,plain,
( spl1514_1
| spl1514_2 ),
inference(sat_conversion,[],[f49155]) ).
cnf(s345,plain,
( ~ spl1514_2
| ~ spl1514_279
| ~ spl1514_280 ),
inference(sat_conversion,[],[f56263]) ).
cnf(s393,plain,
( ~ spl1514_1
| ~ spl1514_279
| ~ spl1514_311 ),
inference(sat_conversion,[],[f56658]) ).
cnf(s2841,plain,
spl1514_408,
inference(sat_conversion,[],[f71491]) ).
cnf(s2846,plain,
spl1514_380,
inference(sat_conversion,[],[f71523]) ).
cnf(s2858,plain,
spl1514_362,
inference(sat_conversion,[],[f71575]) ).
cnf(s57395,plain,
( spl1514_280
| ~ spl1514_380 ),
inference(sat_conversion,[],[f274843]) ).
cnf(s57397,plain,
( ~ spl1514_280
| spl1514_311 ),
inference(sat_conversion,[],[f275025]) ).
cnf(s57398,plain,
( spl1514_279
| ~ spl1514_311
| ~ spl1514_362
| ~ spl1514_408 ),
inference(sat_conversion,[],[f275028]) ).
cnf(s57434,plain,
spl1514_280,
inference(rat,[],[s57395,s2846]) ).
cnf(s57435,plain,
spl1514_311,
inference(rat,[],[s57397,s57434]) ).
cnf(s57438,plain,
spl1514_279,
inference(rat,[],[s57398,s57435,s2858,s2841]) ).
cnf(s57468,plain,
~ spl1514_1,
inference(rat,[],[s393,s57435,s57438]) ).
cnf(s57484,plain,
~ spl1514_2,
inference(rat,[],[s345,s57434,s57438]) ).
cnf(s57577,plain,
$false,
inference(rat,[],[s1,s57484,s57468]) ).
fof(f275029,plain,
$false,
inference(avatar_sat_refutation,[],[s57577]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR082+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 % Computer : n007.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 22:30:41 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.24 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
% 19.83/3.45 % (2929420)Will run a generic schedule for satisfiability detection.
% 19.83/3.45 % (2929427)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=5508307:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi)
% 19.83/3.45 % (2929426)% WARNING: option uhcvi not known.
% 19.83/3.45 % (2929425)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1233339009_2995 on theBenchmark for (2995ds/0Mi)
% 19.83/3.45 % (2929426)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1890573421:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi)
% 19.83/3.45 % (2929428)dis+10_1_sil=32000:sp=arity:random_seed=2467433461:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi)
% 19.83/3.45 % (2929430)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2666985771:i=131_2995 on theBenchmark for (2995ds/131Mi)
% 19.83/3.45 % (2929431)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2027633695:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi)
% 19.83/3.45 % (2929429)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1406094718:i=116_2995 on theBenchmark for (2995ds/116Mi)
% 19.83/3.45 % (2929428)Instruction limit reached!
% 19.83/3.45 % (2929428)------------------------------
% 19.83/3.45 % (2929428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.45 % (2929428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.45 % (2929428)CaDiCaL version: 2.1.3
% 19.83/3.45 % (2929428)Termination reason: Instruction limit
% 19.83/3.45 % (2929428)Termination phase: Preprocessing 3
% 19.83/3.45 % (2929428)Time elapsed: 0.075 s
% 19.83/3.45 % (2929428)Peak memory usage: 36 MB
% 19.83/3.45 % (2929428)Instructions burned: 103 (million)
% 19.83/3.45 % (2929429)Instruction limit reached!
% 19.83/3.45 % (2929429)------------------------------
% 19.83/3.45 % (2929429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.45 % (2929429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.45 % (2929429)CaDiCaL version: 2.1.3
% 19.83/3.45 % (2929429)Termination reason: Instruction limit
% 19.83/3.45 % (2929429)Termination phase: NewCNF
% 19.83/3.45 % (2929429)Time elapsed: 0.087 s
% 19.83/3.45 % (2929429)Peak memory usage: 38 MB
% 19.83/3.45 % (2929429)Instructions burned: 116 (million)
% 19.83/3.45 % (2929430)Instruction limit reached!
% 19.83/3.45 % (2929430)------------------------------
% 19.83/3.45 % (2929430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.45 % (2929430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.45 % (2929430)CaDiCaL version: 2.1.3
% 19.83/3.45 % (2929430)Termination reason: Instruction limit
% 19.83/3.45 % (2929430)Termination phase: Preprocessing 3
% 19.83/3.45 % (2929430)Time elapsed: 0.093 s
% 19.83/3.45 % (2929430)Peak memory usage: 36 MB
% 19.83/3.45 % (2929430)Instructions burned: 132 (million)
% 19.83/3.45 % (2929439)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2038380206:i=714:nm=2_2994 on theBenchmark for (2994ds/714Mi)
% 19.83/3.45 % (2929431)Instruction limit reached!
% 19.83/3.45 % (2929431)------------------------------
% 19.83/3.45 % (2929431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.45 % (2929431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.45 % (2929431)CaDiCaL version: 2.1.3
% 19.83/3.45 % (2929431)Termination reason: Instruction limit
% 19.83/3.45 % (2929431)Termination phase: Preprocessing 3
% 19.83/3.45 % (2929431)Time elapsed: 0.105 s
% 19.83/3.45 % (2929431)Peak memory usage: 38 MB
% 19.83/3.45 % (2929431)Instructions burned: 160 (million)
% 19.83/3.45 % (2929441)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3944965269:i=131:bd=preordered:fsd=on_2994 on theBenchmark for (2994ds/131Mi)
% 19.83/3.45 % (2929442)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=327184220:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2994 on theBenchmark for (2994ds/684Mi)
% 19.83/3.45 % (2929443)ott-21_1_sil=16000:fs=off:random_seed=2029502515:i=180:av=off:fsr=off_2994 on theBenchmark for (2994ds/180Mi)
% 19.83/3.45 % (2929441)Instruction limit reached!
% 19.83/3.45 % (2929441)------------------------------
% 19.83/3.45 % (2929441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.45 % (2929441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929441)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929441)Termination reason: Instruction limit
% 27.90/4.63 % (2929441)Termination phase: Preprocessing 3
% 27.90/4.63 % (2929441)Time elapsed: 0.087 s
% 27.90/4.63 % (2929441)Peak memory usage: 36 MB
% 27.90/4.63 % (2929441)Instructions burned: 132 (million)
% 27.90/4.63 % (2929447)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1154849055:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi)
% 27.90/4.63 % (2929443)Instruction limit reached!
% 27.90/4.63 % (2929443)------------------------------
% 27.90/4.63 % (2929443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929443)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929443)Termination reason: Instruction limit
% 27.90/4.63 % (2929443)Termination phase: Preprocessing 3
% 27.90/4.63 % (2929443)Time elapsed: 0.118 s
% 27.90/4.63 % (2929443)Peak memory usage: 38 MB
% 27.90/4.63 % (2929443)Instructions burned: 181 (million)
% 27.90/4.63 % (2929449)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=947029882:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 27.90/4.63 % (2929442)Instruction limit reached!
% 27.90/4.63 % (2929442)------------------------------
% 27.90/4.63 % (2929442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929442)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929442)Termination reason: Instruction limit
% 27.90/4.63 % (2929442)Termination phase: Saturation
% 27.90/4.63 % (2929442)Time elapsed: 0.364 s
% 27.90/4.63 % (2929442)Peak memory usage: 46 MB
% 27.90/4.63 % (2929442)Instructions burned: 684 (million)
% 27.90/4.63 % (2929439)Instruction limit reached!
% 27.90/4.63 % (2929439)------------------------------
% 27.90/4.63 % (2929439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929439)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929439)Termination reason: Instruction limit
% 27.90/4.63 % (2929439)Termination phase: Property scanning
% 27.90/4.63 % (2929439)Time elapsed: 0.387 s
% 27.90/4.63 % (2929439)Peak memory usage: 73 MB
% 27.90/4.63 % (2929439)Instructions burned: 715 (million)
% 27.90/4.63 % (2929447)Instruction limit reached!
% 27.90/4.63 % (2929447)------------------------------
% 27.90/4.63 % (2929447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929447)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929447)Termination reason: Instruction limit
% 27.90/4.63 % (2929447)Termination phase: Saturation
% 27.90/4.63 % (2929447)Time elapsed: 0.268 s
% 27.90/4.63 % (2929447)Peak memory usage: 43 MB
% 27.90/4.63 % (2929447)Instructions burned: 478 (million)
% 27.90/4.63 % (2929451)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2886897188:i=1179_2990 on theBenchmark for (2990ds/1179Mi)
% 27.90/4.63 % (2929452)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=315904481:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 27.90/4.63 % (2929453)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=1594486415:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 27.90/4.63 % (2929449)Instruction limit reached!
% 27.90/4.63 % (2929449)------------------------------
% 27.90/4.63 % (2929449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.90/4.63 % (2929449)CaDiCaL version: 2.1.3
% 27.90/4.63 % (2929449)Termination reason: Instruction limit
% 27.90/4.63 % (2929449)Termination phase: Property scanning
% 27.90/4.63 % (2929449)Time elapsed: 0.451 s
% 27.90/4.63 % (2929449)Peak memory usage: 71 MB
% 27.90/4.63 % (2929449)Instructions burned: 865 (million)
% 27.90/4.63 % (2929457)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1251047236:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 27.90/4.63 % (2929453)Instruction limit reached!
% 27.90/4.63 % (2929453)------------------------------
% 27.90/4.63 % (2929453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.90/4.63 % (2929453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929453)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929453)Termination reason: Instruction limit
% 48.29/7.44 % (2929453)Termination phase: Saturation
% 48.29/7.44 % (2929453)Time elapsed: 0.366 s
% 48.29/7.44 % (2929453)Peak memory usage: 49 MB
% 48.29/7.44 % (2929453)Instructions burned: 694 (million)
% 48.29/7.44 % (2929459)fmb+10_1_sil=64000:random_seed=1928311018:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 48.29/7.44 % (2929452)Instruction limit reached!
% 48.29/7.44 % (2929452)------------------------------
% 48.29/7.44 % (2929452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929452)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929452)Termination reason: Instruction limit
% 48.29/7.44 % (2929452)Termination phase: Property scanning
% 48.29/7.44 % (2929452)Time elapsed: 0.450 s
% 48.29/7.44 % (2929452)Peak memory usage: 71 MB
% 48.29/7.44 % (2929452)Instructions burned: 890 (million)
% 48.29/7.44 % (2929461)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=106396938:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 48.29/7.44 % (2929451)Instruction limit reached!
% 48.29/7.44 % (2929451)------------------------------
% 48.29/7.44 % (2929451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929451)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929451)Termination reason: Instruction limit
% 48.29/7.44 % (2929451)Termination phase: Saturation
% 48.29/7.44 % (2929451)Time elapsed: 0.641 s
% 48.29/7.44 % (2929451)Peak memory usage: 54 MB
% 48.29/7.44 % (2929451)Instructions burned: 1180 (million)
% 48.29/7.44 % (2929463)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1740197203:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 48.29/7.44 % (2929457)Instruction limit reached!
% 48.29/7.44 % (2929457)------------------------------
% 48.29/7.44 % (2929457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929457)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929457)Termination reason: Instruction limit
% 48.29/7.44 % (2929457)Termination phase: Saturation
% 48.29/7.44 % (2929457)Time elapsed: 0.467 s
% 48.29/7.44 % (2929457)Peak memory usage: 58 MB
% 48.29/7.44 % (2929457)Instructions burned: 881 (million)
% 48.29/7.44 % (2929465)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1143063388:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 48.29/7.44 % (2929463)Instruction limit reached!
% 48.29/7.44 % (2929463)------------------------------
% 48.29/7.44 % (2929463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929463)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929463)Termination reason: Instruction limit
% 48.29/7.44 % (2929463)Termination phase: Property scanning
% 48.29/7.44 % (2929463)Time elapsed: 0.483 s
% 48.29/7.44 % (2929463)Peak memory usage: 71 MB
% 48.29/7.44 % (2929463)Instructions burned: 922 (million)
% 48.29/7.44 % (2929467)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4214302095:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 48.29/7.44 % (2929467)Instruction limit reached!
% 48.29/7.44 % (2929467)------------------------------
% 48.29/7.44 % (2929467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.29/7.44 % (2929467)CaDiCaL version: 2.1.3
% 48.29/7.44 % (2929467)Termination reason: Instruction limit
% 48.29/7.44 % (2929467)Termination phase: Saturation
% 48.29/7.44 % (2929467)Time elapsed: 0.825 s
% 48.29/7.44 % (2929467)Peak memory usage: 60 MB
% 48.29/7.44 % (2929467)Instructions burned: 1476 (million)
% 48.29/7.44 % (2929469)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1232180257:i=6324_2970 on theBenchmark for (2970ds/6324Mi)
% 48.29/7.44 % Detected minimum model sizes of [447]
% 48.29/7.44 % Detected maximum model sizes of [max]
% 48.29/7.44 % (2929425)Cannot represent all propositional literals internally
% 48.29/7.44 % (2929425)Refutation not found, incomplete strategy
% 48.29/7.44 % (2929425)------------------------------
% 48.29/7.44 % (2929425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.29/7.44 % (2929425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929425)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929425)Termination reason: Refutation not found, incomplete strategy
% 76.84/11.49 % (2929425)Time elapsed: 2.778 s
% 76.84/11.49 % (2929425)Peak memory usage: 149 MB
% 76.84/11.49 % (2929425)Instructions burned: 5805 (million)
% 76.84/11.49 % (2929425)------------------------------
% 76.84/11.49 % (2929425)------------------------------
% 76.84/11.49 % (2929471)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1140033288:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 76.84/11.49 % Detected minimum model sizes of [447]
% 76.84/11.49 % Detected maximum model sizes of [max]
% 76.84/11.49 % (2929459)Cannot represent all propositional literals internally
% 76.84/11.49 % (2929459)Refutation not found, incomplete strategy
% 76.84/11.49 % (2929459)------------------------------
% 76.84/11.49 % (2929459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.84/11.49 % (2929459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929459)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929459)Termination reason: Refutation not found, incomplete strategy
% 76.84/11.49 % (2929459)Time elapsed: 2.325 s
% 76.84/11.49 % (2929459)Peak memory usage: 132 MB
% 76.84/11.49 % (2929459)Instructions burned: 5026 (million)
% 76.84/11.49 % (2929459)------------------------------
% 76.84/11.49 % (2929459)------------------------------
% 76.84/11.49 % (2929473)ott-2_1_sil=16000:newcnf=on:random_seed=1910662702:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2962 on theBenchmark for (2962ds/869Mi)
% 76.84/11.49 % Detected minimum model sizes of [447]
% 76.84/11.49 % Detected maximum model sizes of [max]
% 76.84/11.49 % (2929461)Cannot represent all propositional literals internally
% 76.84/11.49 % (2929461)Refutation not found, incomplete strategy
% 76.84/11.49 % (2929461)------------------------------
% 76.84/11.49 % (2929461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.84/11.49 % (2929461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929461)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929461)Termination reason: Refutation not found, incomplete strategy
% 76.84/11.49 % (2929461)Time elapsed: 2.418 s
% 76.84/11.49 % (2929461)Peak memory usage: 137 MB
% 76.84/11.49 % (2929461)Instructions burned: 5225 (million)
% 76.84/11.49 % (2929461)------------------------------
% 76.84/11.49 % (2929461)------------------------------
% 76.84/11.49 % (2929475)ott+10_1_sil=32000:tgt=ground:random_seed=1158027645:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 76.84/11.49 % (2929473)Instruction limit reached!
% 76.84/11.49 % (2929473)------------------------------
% 76.84/11.49 % (2929473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.84/11.49 % (2929473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929473)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929473)Termination reason: Instruction limit
% 76.84/11.49 % (2929473)Termination phase: Saturation
% 76.84/11.49 % (2929473)Time elapsed: 0.453 s
% 76.84/11.49 % (2929473)Peak memory usage: 50 MB
% 76.84/11.49 % (2929473)Instructions burned: 870 (million)
% 76.84/11.49 % (2929477)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=793505877:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 76.84/11.49 % (2929471)Instruction limit reached!
% 76.84/11.49 % (2929471)------------------------------
% 76.84/11.49 % (2929471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.84/11.49 % (2929471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929471)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929471)Termination reason: Instruction limit
% 76.84/11.49 % (2929471)Termination phase: Finite model building preprocessing
% 76.84/11.49 % (2929471)Time elapsed: 1.080 s
% 76.84/11.49 % (2929471)Peak memory usage: 110 MB
% 76.84/11.49 % (2929471)Instructions burned: 2175 (million)
% 76.84/11.49 % (2929465)Instruction limit reached!
% 76.84/11.49 % (2929465)------------------------------
% 76.84/11.49 % (2929465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.84/11.49 % (2929465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.84/11.49 % (2929465)CaDiCaL version: 2.1.3
% 76.84/11.49 % (2929465)Termination reason: Instruction limit
% 76.84/11.49 % (2929465)Termination phase: Saturation
% 76.84/11.49 % (2929465)Time elapsed: 2.679 s
% 76.84/11.49 % (2929465)Peak memory usage: 95 MB
% 76.84/11.49 % (2929465)Instructions burned: 5131 (million)
% 76.84/11.49 % (2929479)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=254251339:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 143.23/24.36 % (2929480)dis+21_1_sil=32000:sas=cadical:random_seed=1832062487:i=3773:amm=off_2956 on theBenchmark for (2956ds/3773Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929469)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929469)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929469)------------------------------
% 143.23/24.36 % (2929469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929469)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929469)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929469)Time elapsed: 2.755 s
% 143.23/24.36 % (2929469)Peak memory usage: 147 MB
% 143.23/24.36 % (2929469)Instructions burned: 5785 (million)
% 143.23/24.36 % (2929469)------------------------------
% 143.23/24.36 % (2929469)------------------------------
% 143.23/24.36 % (2929483)ott+11_1_sil=16000:gs=on:random_seed=3678665508:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 143.23/24.36 % (2929480)Instruction limit reached!
% 143.23/24.36 % (2929480)------------------------------
% 143.23/24.36 % (2929480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929480)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929480)Termination reason: Instruction limit
% 143.23/24.36 % (2929480)Termination phase: Saturation
% 143.23/24.36 % (2929480)Time elapsed: 1.613 s
% 143.23/24.36 % (2929480)Peak memory usage: 67 MB
% 143.23/24.36 % (2929480)Instructions burned: 3776 (million)
% 143.23/24.36 % (2929485)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2635078393:fmbsr=1.6:i=67534_2939 on theBenchmark for (2939ds/67534Mi)
% 143.23/24.36 % (2929479)Instruction limit reached!
% 143.23/24.36 % (2929479)------------------------------
% 143.23/24.36 % (2929479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929479)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929479)Termination reason: Instruction limit
% 143.23/24.36 % (2929479)Termination phase: Saturation
% 143.23/24.36 % (2929479)Time elapsed: 1.840 s
% 143.23/24.36 % (2929479)Peak memory usage: 106 MB
% 143.23/24.36 % (2929479)Instructions burned: 3513 (million)
% 143.23/24.36 % (2929487)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3397245745:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi)
% 143.23/24.36 % (2929475)Instruction limit reached!
% 143.23/24.36 % (2929475)------------------------------
% 143.23/24.36 % (2929475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929475)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929475)Termination reason: Instruction limit
% 143.23/24.36 % (2929475)Termination phase: Saturation
% 143.23/24.36 % (2929475)Time elapsed: 2.814 s
% 143.23/24.36 % (2929475)Peak memory usage: 76 MB
% 143.23/24.36 % (2929475)Instructions burned: 5115 (million)
% 143.23/24.36 % (2929489)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1382138889:i=29340_2932 on theBenchmark for (2932ds/29340Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929477)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929477)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929477)------------------------------
% 143.23/24.36 % (2929477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929477)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929477)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929477)Time elapsed: 2.737 s
% 143.23/24.36 % (2929477)Peak memory usage: 148 MB
% 143.23/24.36 % (2929477)Instructions burned: 5805 (million)
% 143.23/24.36 % (2929477)------------------------------
% 143.23/24.36 % (2929477)------------------------------
% 143.23/24.36 % (2929491)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3430447071:i=5211_2929 on theBenchmark for (2929ds/5211Mi)
% 143.23/24.36 % (2929483)Instruction limit reached!
% 143.23/24.36 % (2929483)------------------------------
% 143.23/24.36 % (2929483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929483)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929483)Termination reason: Instruction limit
% 143.23/24.36 % (2929483)Termination phase: Saturation
% 143.23/24.36 % (2929483)Time elapsed: 1.382 s
% 143.23/24.36 % (2929483)Peak memory usage: 85 MB
% 143.23/24.36 % (2929483)Instructions burned: 2252 (million)
% 143.23/24.36 % (2929493)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2743828596:i=5497:nm=2_2927 on theBenchmark for (2927ds/5497Mi)
% 143.23/24.36 % (2929487)Instruction limit reached!
% 143.23/24.36 % (2929487)------------------------------
% 143.23/24.36 % (2929487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929487)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929487)Termination reason: Instruction limit
% 143.23/24.36 % (2929487)Termination phase: Saturation
% 143.23/24.36 % (2929487)Time elapsed: 2.294 s
% 143.23/24.36 % (2929487)Peak memory usage: 70 MB
% 143.23/24.36 % (2929487)Instructions burned: 4591 (million)
% 143.23/24.36 % (2929495)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=623784558:fmbsr=2:i=46332_2914 on theBenchmark for (2914ds/46332Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929485)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929485)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929485)------------------------------
% 143.23/24.36 % (2929485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929485)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929485)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929485)Time elapsed: 2.623 s
% 143.23/24.36 % (2929485)Peak memory usage: 141 MB
% 143.23/24.36 % (2929485)Instructions burned: 5798 (million)
% 143.23/24.36 % (2929485)------------------------------
% 143.23/24.36 % (2929485)------------------------------
% 143.23/24.36 % (2929497)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=662351111:i=14071_2912 on theBenchmark for (2912ds/14071Mi)
% 143.23/24.36 % (2929491)Instruction limit reached!
% 143.23/24.36 % (2929491)------------------------------
% 143.23/24.36 % (2929491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929491)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929491)Termination reason: Instruction limit
% 143.23/24.36 % (2929491)Termination phase: Saturation
% 143.23/24.36 % (2929491)Time elapsed: 2.404 s
% 143.23/24.36 % (2929491)Peak memory usage: 70 MB
% 143.23/24.36 % (2929491)Instructions burned: 5213 (million)
% 143.23/24.36 % (2929499)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3759040552:i=22565:add=on:rawr=on_2905 on theBenchmark for (2905ds/22565Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929493)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929493)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929493)------------------------------
% 143.23/24.36 % (2929493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929493)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929493)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929493)Time elapsed: 2.622 s
% 143.23/24.36 % (2929493)Peak memory usage: 141 MB
% 143.23/24.36 % (2929493)Instructions burned: 5384 (million)
% 143.23/24.36 % (2929493)------------------------------
% 143.23/24.36 % (2929493)------------------------------
% 143.23/24.36 % (2929501)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2820617906:i=8173:av=off_2901 on theBenchmark for (2901ds/8173Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929497)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929497)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929497)------------------------------
% 143.23/24.36 % (2929497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929497)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929497)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929497)Time elapsed: 2.508 s
% 143.23/24.36 % (2929497)Peak memory usage: 139 MB
% 143.23/24.36 % (2929497)Instructions burned: 5350 (million)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929495)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929495)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929495)------------------------------
% 143.23/24.36 % (2929495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929495)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929495)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929495)Time elapsed: 2.656 s
% 143.23/24.36 % (2929495)Peak memory usage: 141 MB
% 143.23/24.36 % (2929495)Instructions burned: 5798 (million)
% 143.23/24.36 % (2929497)------------------------------
% 143.23/24.36 % (2929497)------------------------------
% 143.23/24.36 % (2929495)------------------------------
% 143.23/24.36 % (2929495)------------------------------
% 143.23/24.36 % (2929503)dis+10_16:1_sil=16000:random_seed=2968335762:i=9155:fsr=off_2887 on theBenchmark for (2887ds/9155Mi)
% 143.23/24.36 % (2929504)ott-3_8_sil=64000:random_seed=3436848537:i=20139:bs=on_2887 on theBenchmark for (2887ds/20139Mi)
% 143.23/24.36 % (2929501)Instruction limit reached!
% 143.23/24.36 % (2929501)------------------------------
% 143.23/24.36 % (2929501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929501)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929501)Termination reason: Instruction limit
% 143.23/24.36 % (2929501)Termination phase: Saturation
% 143.23/24.36 % (2929501)Time elapsed: 5.024 s
% 143.23/24.36 % (2929501)Peak memory usage: 93 MB
% 143.23/24.36 % (2929501)Instructions burned: 8173 (million)
% 143.23/24.36 % (2929775)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1937482216:fmbsr=2:i=32576_2850 on theBenchmark for (2850ds/32576Mi)
% 143.23/24.36 % (2929503)Instruction limit reached!
% 143.23/24.36 % (2929503)------------------------------
% 143.23/24.36 % (2929503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929503)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929503)Termination reason: Instruction limit
% 143.23/24.36 % (2929503)Termination phase: Saturation
% 143.23/24.36 % (2929503)Time elapsed: 4.816 s
% 143.23/24.36 % (2929503)Peak memory usage: 130 MB
% 143.23/24.36 % (2929503)Instructions burned: 9156 (million)
% 143.23/24.36 % (2929796)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1880488244:i=11404_2838 on theBenchmark for (2838ds/11404Mi)
% 143.23/24.36 % Detected minimum model sizes of [447]
% 143.23/24.36 % Detected maximum model sizes of [max]
% 143.23/24.36 % (2929775)Cannot represent all propositional literals internally
% 143.23/24.36 % (2929775)Refutation not found, incomplete strategy
% 143.23/24.36 % (2929775)------------------------------
% 143.23/24.36 % (2929775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.36 % (2929775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.36 % (2929775)CaDiCaL version: 2.1.3
% 143.23/24.36 % (2929775)Termination reason: Refutation not found, incomplete strategy
% 143.23/24.36 % (2929775)Time elapsed: 4.136 s
% 143.23/24.36 % (2929775)Peak memory usage: 147 MB
% 143.23/24.36 % (2929775)Instructions burned: 5788 (million)
% 143.23/24.36 % (2929775)------------------------------
% 143.23/24.36 % (2929775)------------------------------
% 143.23/24.36 % (2929832)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2137086662:i=14134_2807 on theBenchmark for (2807ds/14134Mi)
% 143.23/24.36 % (2929832) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2929420-2929832"...
% 143.23/24.36 % (2929832)...printing done.
% 143.23/24.36 % (2929832)Refutation found. Thanks to Tanya!
% 143.23/24.36 % SZS status Theorem for theBenchmark
% 143.23/24.36 % SZS output start Proof for theBenchmark
% See solution above
% 143.23/24.38 % (2929832)------------------------------
% 143.23/24.38 % (2929832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.23/24.38 % (2929832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.23/24.38 % (2929832)CaDiCaL version: 2.1.3
% 143.23/24.38 % (2929832)Termination reason: Refutation
% 143.23/24.38 % (2929832)Time elapsed: 4.461 s
% 143.23/24.38 % (2929832)Peak memory usage: 125 MB
% 143.23/24.38 % (2929832)Instructions burned: 7515 (million)
% 143.23/24.38 % (2929420)Success in time 24.112 s
% 143.23/24.38 % Vampire exiting
%------------------------------------------------------------------------------