%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR079+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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:01 AM UTC 2026
% Result : Theorem 76.77s 18.98s
% Output : Refutation 76.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 23
% Syntax : Number of formulae : 94 ( 53 unt; 2 def)
% Number of atoms : 196 ( 26 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 178 ( 76 ~; 72 |; 22 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 21 con; 0-1 aty)
% Number of variables : 47 ( 0 sgn 43 !; 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(f7048,axiom,
s__subclass(s__OrganicObject,s__CorpuscularObject),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7121) ).
fof(f7055,axiom,
s__subclass(s__Organism,s__OrganicObject),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7128) ).
fof(f7146,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7220) ).
fof(f7220,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7294) ).
fof(f11141,axiom,
! [X0] :
( s__instance(X0,s__CorpuscularObject)
=> ( s__instance(X0,s__Vertebrate)
<=> ? [X1] :
( s__instance(X1,s__CorpuscularObject)
& s__instance(X0,s__Animal)
& s__component(X1,X0)
& s__instance(X1,s__SpinalColumn) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_11284) ).
fof(f16750,axiom,
s__instance(s__Organism5_1,s__Lizard5_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f16770,axiom,
s__subclass(s__Class5_10,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_22) ).
fof(f16771,axiom,
s__Class5_1 = s__Class5_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_23) ).
fof(f16772,axiom,
s__Class5_2 = s__Class5_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_24) ).
fof(f16773,axiom,
s__Class5_3 = s__Class5_4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_25) ).
fof(f16774,axiom,
s__Class5_4 = s__Class5_5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_26) ).
fof(f16775,axiom,
s__Class5_5 = s__Class5_6,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_27) ).
fof(f16776,axiom,
s__Class5_6 = s__Class5_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_28) ).
fof(f16777,axiom,
s__Class5_7 = s__Class5_8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_29) ).
fof(f16778,axiom,
s__Class5_8 = s__Class5_9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_30) ).
fof(f16779,axiom,
s__Class5_9 = s__Class5_10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_31) ).
fof(f16780,axiom,
s__subclass(s__Lizard5_1,s__Class5_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_32) ).
fof(f16781,axiom,
s__subclass(s__Class5_10,s__Reptile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_33) ).
fof(f16782,conjecture,
s__instance(s__Organism5_1,s__Animal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f16783,negated_conjecture,
~ s__instance(s__Organism5_1,s__Animal),
inference(negated_conjecture,[status(cth)],[f16782]) ).
fof(f16796,plain,
~ s__instance(s__Organism5_1,s__Animal),
inference(flattening,[],[f16783]) ).
fof(f17051,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f17052,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(f17053,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,[],[f17052]) ).
fof(f25406,plain,
! [X0] :
( ( s__instance(X0,s__Vertebrate)
<=> ? [X1] :
( s__instance(X1,s__CorpuscularObject)
& s__instance(X0,s__Animal)
& s__component(X1,X0)
& s__instance(X1,s__SpinalColumn) ) )
| ~ s__instance(X0,s__CorpuscularObject) ),
inference(ennf_transformation,[],[f11141]) ).
fof(f28186,plain,
! [X0] :
( ( ( s__instance(X0,s__Vertebrate)
| ! [X1] :
( ~ s__instance(X1,s__CorpuscularObject)
| ~ s__instance(X0,s__Animal)
| ~ s__component(X1,X0)
| ~ s__instance(X1,s__SpinalColumn) ) )
& ( ? [X1] :
( s__instance(X1,s__CorpuscularObject)
& s__instance(X0,s__Animal)
& s__component(X1,X0)
& s__instance(X1,s__SpinalColumn) )
| ~ s__instance(X0,s__Vertebrate) ) )
| ~ s__instance(X0,s__CorpuscularObject) ),
inference(nnf_transformation,[],[f25406]) ).
fof(f28187,plain,
! [X0] :
( ( ( s__instance(X0,s__Vertebrate)
| ! [X1] :
( ~ s__instance(X1,s__CorpuscularObject)
| ~ s__instance(X0,s__Animal)
| ~ s__component(X1,X0)
| ~ s__instance(X1,s__SpinalColumn) ) )
& ( ? [X2] :
( s__instance(X2,s__CorpuscularObject)
& s__instance(X0,s__Animal)
& s__component(X2,X0)
& s__instance(X2,s__SpinalColumn) )
| ~ s__instance(X0,s__Vertebrate) ) )
| ~ s__instance(X0,s__CorpuscularObject) ),
inference(rectify,[],[f28186]) ).
fof(f28188,plain,
! [X0] :
( ( ( s__instance(X0,s__Vertebrate)
| ! [X1] :
( ~ s__instance(X1,s__CorpuscularObject)
| ~ s__instance(X0,s__Animal)
| ~ s__component(X1,X0)
| ~ s__instance(X1,s__SpinalColumn) ) )
& ( ( s__instance(sK925(X0),s__CorpuscularObject)
& s__instance(X0,s__Animal)
& s__component(sK925(X0),X0)
& s__instance(sK925(X0),s__SpinalColumn) )
| ~ s__instance(X0,s__Vertebrate) ) )
| ~ s__instance(X0,s__CorpuscularObject) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK925]),skolemize(X2,sK925(X0))],[f28187]) ).
fof(f28711,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17051]) ).
fof(f28712,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17051]) ).
fof(f28713,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,[],[f17053]) ).
fof(f36562,plain,
s__subclass(s__OrganicObject,s__CorpuscularObject),
inference(cnf_transformation,[],[f7048]) ).
fof(f36569,plain,
s__subclass(s__Organism,s__OrganicObject),
inference(cnf_transformation,[],[f7055]) ).
fof(f36669,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f7146]) ).
fof(f36745,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f7220]) ).
fof(f41713,plain,
! [X0] :
( s__instance(X0,s__Animal)
| ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__CorpuscularObject) ),
inference(cnf_transformation,[],[f28188]) ).
fof(f48609,plain,
s__instance(s__Organism5_1,s__Lizard5_1),
inference(cnf_transformation,[],[f16750]) ).
fof(f48629,plain,
s__subclass(s__Class5_10,s__Organism),
inference(cnf_transformation,[],[f16770]) ).
fof(f48630,plain,
s__Class5_1 = s__Class5_2,
inference(cnf_transformation,[],[f16771]) ).
fof(f48631,plain,
s__Class5_2 = s__Class5_3,
inference(cnf_transformation,[],[f16772]) ).
fof(f48632,plain,
s__Class5_3 = s__Class5_4,
inference(cnf_transformation,[],[f16773]) ).
fof(f48633,plain,
s__Class5_4 = s__Class5_5,
inference(cnf_transformation,[],[f16774]) ).
fof(f48634,plain,
s__Class5_5 = s__Class5_6,
inference(cnf_transformation,[],[f16775]) ).
fof(f48635,plain,
s__Class5_6 = s__Class5_7,
inference(cnf_transformation,[],[f16776]) ).
fof(f48636,plain,
s__Class5_7 = s__Class5_8,
inference(cnf_transformation,[],[f16777]) ).
fof(f48637,plain,
s__Class5_8 = s__Class5_9,
inference(cnf_transformation,[],[f16778]) ).
fof(f48638,plain,
s__Class5_9 = s__Class5_10,
inference(cnf_transformation,[],[f16779]) ).
fof(f48639,plain,
s__subclass(s__Lizard5_1,s__Class5_1),
inference(cnf_transformation,[],[f16780]) ).
fof(f48640,plain,
s__subclass(s__Class5_10,s__Reptile),
inference(cnf_transformation,[],[f16781]) ).
fof(f48641,plain,
~ s__instance(s__Organism5_1,s__Animal),
inference(cnf_transformation,[],[f16796]) ).
fof(f48642,plain,
s__Class5_8 = s__Class5_10,
inference(definition_unfolding,[],[f48637,f48638]) ).
fof(f48643,plain,
s__Class5_7 = s__Class5_10,
inference(definition_unfolding,[],[f48636,f48642]) ).
fof(f48644,plain,
s__Class5_6 = s__Class5_10,
inference(definition_unfolding,[],[f48635,f48643]) ).
fof(f48645,plain,
s__Class5_5 = s__Class5_10,
inference(definition_unfolding,[],[f48634,f48644]) ).
fof(f48646,plain,
s__Class5_4 = s__Class5_10,
inference(definition_unfolding,[],[f48633,f48645]) ).
fof(f48647,plain,
s__Class5_3 = s__Class5_10,
inference(definition_unfolding,[],[f48632,f48646]) ).
fof(f48648,plain,
s__Class5_2 = s__Class5_10,
inference(definition_unfolding,[],[f48631,f48647]) ).
fof(f48649,plain,
s__Class5_1 = s__Class5_10,
inference(definition_unfolding,[],[f48630,f48648]) ).
fof(f48668,plain,
s__subclass(s__Lizard5_1,s__Class5_10),
inference(definition_unfolding,[],[f48639,f48649]) ).
fof(f61965,plain,
( ~ s__instance(s__Organism5_1,s__Vertebrate)
| ~ s__instance(s__Organism5_1,s__CorpuscularObject) ),
inference(resolution,[],[f41713,f48641]) ).
fof(f61967,definition,
( spl1514_771
<=> s__instance(s__Organism5_1,s__CorpuscularObject) ),
introduced(definition,[new_symbols(definition,[spl1514_771])],[avatar_definition]) ).
fof(f61969,plain,
( ~ s__instance(s__Organism5_1,s__CorpuscularObject)
| spl1514_771 ),
inference(avatar_component_clause,[],[f61967]) ).
fof(f61971,definition,
( spl1514_772
<=> s__instance(s__Organism5_1,s__Vertebrate) ),
introduced(definition,[new_symbols(definition,[spl1514_772])],[avatar_definition]) ).
fof(f61973,plain,
( ~ s__instance(s__Organism5_1,s__Vertebrate)
| spl1514_772 ),
inference(avatar_component_clause,[],[f61971]) ).
fof(f61974,plain,
( ~ spl1514_771
| ~ spl1514_772 ),
inference(avatar_split_clause,[],[f61965,f61971,f61967]) ).
fof(f64455,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f28713,f28711]) ).
fof(f64513,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f64455,f28712]) ).
fof(f97904,plain,
( ! [X0] :
( ~ s__subclass(X0,s__CorpuscularObject)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_771 ),
inference(resolution,[],[f64513,f61969]) ).
fof(f97949,plain,
( ~ s__instance(s__Organism5_1,s__OrganicObject)
| spl1514_771 ),
inference(resolution,[],[f97904,f36562]) ).
fof(f97954,plain,
( ! [X0] :
( ~ s__subclass(X0,s__OrganicObject)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_771 ),
inference(resolution,[],[f97949,f64513]) ).
fof(f98003,plain,
( ~ s__instance(s__Organism5_1,s__Organism)
| spl1514_771 ),
inference(resolution,[],[f97954,f36569]) ).
fof(f98007,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Organism)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_771 ),
inference(resolution,[],[f98003,f64513]) ).
fof(f98151,plain,
( ~ s__instance(s__Organism5_1,s__Class5_10)
| spl1514_771 ),
inference(resolution,[],[f98007,f48629]) ).
fof(f98155,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Class5_10)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_771 ),
inference(resolution,[],[f98151,f64513]) ).
fof(f98354,plain,
( ~ s__instance(s__Organism5_1,s__Lizard5_1)
| spl1514_771 ),
inference(resolution,[],[f98155,f48668]) ).
fof(f98355,plain,
( $false
| spl1514_771 ),
inference(forward_subsumption_resolution,[],[f98354,f48609]) ).
fof(f98356,plain,
spl1514_771,
inference(avatar_contradiction_clause,[],[f98355]) ).
fof(f98358,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_772 ),
inference(resolution,[],[f61973,f64513]) ).
fof(f98361,plain,
( ~ s__instance(s__Organism5_1,s__ColdBloodedVertebrate)
| spl1514_772 ),
inference(resolution,[],[f98358,f36669]) ).
fof(f98363,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_772 ),
inference(resolution,[],[f98361,f64513]) ).
fof(f98369,plain,
( ~ s__instance(s__Organism5_1,s__Reptile)
| spl1514_772 ),
inference(resolution,[],[f98363,f36745]) ).
fof(f98372,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_772 ),
inference(resolution,[],[f98369,f64513]) ).
fof(f98390,plain,
( ~ s__instance(s__Organism5_1,s__Class5_10)
| spl1514_772 ),
inference(resolution,[],[f98372,f48640]) ).
fof(f98392,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Class5_10)
| ~ s__instance(s__Organism5_1,X0) )
| spl1514_772 ),
inference(resolution,[],[f98390,f64513]) ).
fof(f98436,plain,
( ~ s__instance(s__Organism5_1,s__Lizard5_1)
| spl1514_772 ),
inference(resolution,[],[f98392,f48668]) ).
fof(f98437,plain,
( $false
| spl1514_772 ),
inference(forward_subsumption_resolution,[],[f98436,f48609]) ).
fof(f98438,plain,
spl1514_772,
inference(avatar_contradiction_clause,[],[f98437]) ).
cnf(s3947,plain,
( ~ spl1514_771
| ~ spl1514_772 ),
inference(sat_conversion,[],[f61974]) ).
cnf(s9410,plain,
spl1514_771,
inference(sat_conversion,[],[f98356]) ).
cnf(s9411,plain,
spl1514_772,
inference(sat_conversion,[],[f98438]) ).
cnf(s9415,plain,
$false,
inference(rat,[],[s3947,s9411,s9410]) ).
fof(f98439,plain,
$false,
inference(avatar_sat_refutation,[],[s9415]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR079+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.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:31:37 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 24.53/4.08 % (855464)Will run a generic schedule for satisfiability detection.
% 24.53/4.08 % (855568)dis+10_1_sil=32000:sp=arity:random_seed=2172657803:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi)
% 24.53/4.08 % (855566)% WARNING: option uhcvi not known.
% 24.53/4.08 % (855565)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=306660618_2995 on theBenchmark for (2995ds/0Mi)
% 24.53/4.08 % (855566)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2163731956:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi)
% 24.53/4.08 % (855567)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3557670603:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi)
% 24.53/4.08 % (855569)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=333664420:i=116_2995 on theBenchmark for (2995ds/116Mi)
% 24.53/4.08 % (855571)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2838122101:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi)
% 24.53/4.08 % (855570)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3231765520:i=131_2995 on theBenchmark for (2995ds/131Mi)
% 24.53/4.08 % (855568)Instruction limit reached!
% 24.53/4.08 % (855568)------------------------------
% 24.53/4.08 % (855568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.53/4.08 % (855568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.08 % (855568)CaDiCaL version: 2.1.3
% 24.53/4.08 % (855568)Termination reason: Instruction limit
% 24.53/4.08 % (855568)Termination phase: Preprocessing 3
% 24.53/4.08 % (855568)Time elapsed: 0.048 s
% 24.53/4.08 % (855568)Peak memory usage: 36 MB
% 24.53/4.08 % (855568)Instructions burned: 103 (million)
% 24.53/4.08 % (855588)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4163891435:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 24.53/4.08 % (855569)Instruction limit reached!
% 24.53/4.08 % (855569)------------------------------
% 24.53/4.08 % (855569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.53/4.08 % (855569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.08 % (855569)CaDiCaL version: 2.1.3
% 24.53/4.08 % (855569)Termination reason: Instruction limit
% 24.53/4.08 % (855569)Termination phase: NewCNF
% 24.53/4.08 % (855569)Time elapsed: 0.089 s
% 24.53/4.08 % (855569)Peak memory usage: 38 MB
% 24.53/4.08 % (855569)Instructions burned: 116 (million)
% 24.53/4.08 % (855570)Instruction limit reached!
% 24.53/4.08 % (855570)------------------------------
% 24.53/4.08 % (855570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.53/4.08 % (855570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.08 % (855570)CaDiCaL version: 2.1.3
% 24.53/4.08 % (855570)Termination reason: Instruction limit
% 24.53/4.08 % (855570)Termination phase: Preprocessing 3
% 24.53/4.08 % (855570)Time elapsed: 0.097 s
% 24.53/4.08 % (855570)Peak memory usage: 36 MB
% 24.53/4.08 % (855570)Instructions burned: 132 (million)
% 24.53/4.08 % (855571)Instruction limit reached!
% 24.53/4.08 % (855571)------------------------------
% 24.53/4.08 % (855571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.53/4.08 % (855571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.08 % (855571)CaDiCaL version: 2.1.3
% 24.53/4.08 % (855571)Termination reason: Instruction limit
% 24.53/4.08 % (855571)Termination phase: Preprocessing 3
% 24.53/4.08 % (855571)Time elapsed: 0.106 s
% 24.53/4.08 % (855571)Peak memory usage: 38 MB
% 24.53/4.08 % (855571)Instructions burned: 160 (million)
% 24.53/4.08 % (855604)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1598632310:i=131:bd=preordered:fsd=on_2994 on theBenchmark for (2994ds/131Mi)
% 24.53/4.08 % (855607)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=1809988411:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2994 on theBenchmark for (2994ds/684Mi)
% 24.53/4.08 % (855608)ott-21_1_sil=16000:fs=off:random_seed=3156842574:i=180:av=off:fsr=off_2994 on theBenchmark for (2994ds/180Mi)
% 24.53/4.08 % (855604)Instruction limit reached!
% 24.53/4.08 % (855604)------------------------------
% 24.53/4.08 % (855604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.53/4.08 % (855604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.08 % (855604)CaDiCaL version: 2.1.3
% 24.53/4.08 % (855604)Termination reason: Instruction limit
% 48.43/7.45 % (855604)Termination phase: Preprocessing 3
% 48.43/7.45 % (855604)Time elapsed: 0.086 s
% 48.43/7.45 % (855604)Peak memory usage: 36 MB
% 48.43/7.45 % (855604)Instructions burned: 131 (million)
% 48.43/7.45 % (855621)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3820540386:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi)
% 48.43/7.45 % (855608)Instruction limit reached!
% 48.43/7.45 % (855608)------------------------------
% 48.43/7.45 % (855608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.45 % (855608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.45 % (855608)CaDiCaL version: 2.1.3
% 48.43/7.45 % (855608)Termination reason: Instruction limit
% 48.43/7.45 % (855608)Termination phase: Preprocessing 3
% 48.43/7.45 % (855608)Time elapsed: 0.115 s
% 48.43/7.45 % (855608)Peak memory usage: 38 MB
% 48.43/7.45 % (855608)Instructions burned: 182 (million)
% 48.43/7.45 % (855623)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3250616091:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 48.43/7.45 % (855588)Instruction limit reached!
% 48.43/7.45 % (855588)------------------------------
% 48.43/7.46 % (855588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.46 % (855588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.46 % (855588)CaDiCaL version: 2.1.3
% 48.43/7.46 % (855588)Termination reason: Instruction limit
% 48.43/7.46 % (855588)Termination phase: Property scanning
% 48.43/7.46 % (855588)Time elapsed: 0.417 s
% 48.43/7.46 % (855588)Peak memory usage: 73 MB
% 48.43/7.46 % (855588)Instructions burned: 717 (million)
% 48.43/7.46 % (855607)Instruction limit reached!
% 48.43/7.46 % (855607)------------------------------
% 48.43/7.46 % (855607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.46 % (855607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.46 % (855607)CaDiCaL version: 2.1.3
% 48.43/7.46 % (855607)Termination reason: Instruction limit
% 48.43/7.46 % (855607)Termination phase: Saturation
% 48.43/7.46 % (855607)Time elapsed: 0.355 s
% 48.43/7.46 % (855607)Peak memory usage: 46 MB
% 48.43/7.46 % (855607)Instructions burned: 688 (million)
% 48.43/7.46 % (855621)Instruction limit reached!
% 48.43/7.46 % (855621)------------------------------
% 48.43/7.46 % (855621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.46 % (855621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.46 % (855621)CaDiCaL version: 2.1.3
% 48.43/7.46 % (855621)Termination reason: Instruction limit
% 48.43/7.46 % (855621)Termination phase: Property scanning
% 48.43/7.46 % (855621)Time elapsed: 0.266 s
% 48.43/7.46 % (855621)Peak memory usage: 41 MB
% 48.43/7.46 % (855621)Instructions burned: 477 (million)
% 48.43/7.46 % (855626)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=152907542:i=1179_2990 on theBenchmark for (2990ds/1179Mi)
% 48.43/7.46 % (855627)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1128672931:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 48.43/7.46 % (855628)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=4281143587: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)
% 48.43/7.46 % (855623)Instruction limit reached!
% 48.43/7.46 % (855623)------------------------------
% 48.43/7.46 % (855623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.46 % (855623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.46 % (855623)CaDiCaL version: 2.1.3
% 48.43/7.46 % (855623)Termination reason: Instruction limit
% 48.43/7.46 % (855623)Termination phase: Property scanning
% 48.43/7.46 % (855623)Time elapsed: 0.435 s
% 48.43/7.46 % (855623)Peak memory usage: 71 MB
% 48.43/7.46 % (855623)Instructions burned: 866 (million)
% 48.43/7.46 % (855632)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1373543067:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 48.43/7.46 % (855628)Instruction limit reached!
% 48.43/7.46 % (855628)------------------------------
% 48.43/7.46 % (855628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.43/7.46 % (855628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.43/7.46 % (855628)CaDiCaL version: 2.1.3
% 48.43/7.46 % (855628)Termination reason: Instruction limit
% 48.43/7.46 % (855628)Termination phase: Saturation
% 71.10/10.63 % (855628)Time elapsed: 0.369 s
% 71.10/10.63 % (855628)Peak memory usage: 47 MB
% 71.10/10.63 % (855628)Instructions burned: 694 (million)
% 71.10/10.63 % (855634)fmb+10_1_sil=64000:random_seed=1494471986:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 71.10/10.63 % (855627)Instruction limit reached!
% 71.10/10.63 % (855627)------------------------------
% 71.10/10.63 % (855627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855627)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855627)Termination reason: Instruction limit
% 71.10/10.63 % (855627)Termination phase: Property scanning
% 71.10/10.63 % (855627)Time elapsed: 0.451 s
% 71.10/10.63 % (855627)Peak memory usage: 71 MB
% 71.10/10.63 % (855627)Instructions burned: 891 (million)
% 71.10/10.63 % (855636)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3978893213:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 71.10/10.63 % (855626)Instruction limit reached!
% 71.10/10.63 % (855626)------------------------------
% 71.10/10.63 % (855626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855626)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855626)Termination reason: Instruction limit
% 71.10/10.63 % (855626)Termination phase: Saturation
% 71.10/10.63 % (855626)Time elapsed: 0.652 s
% 71.10/10.63 % (855626)Peak memory usage: 54 MB
% 71.10/10.63 % (855626)Instructions burned: 1180 (million)
% 71.10/10.63 % (855632)Instruction limit reached!
% 71.10/10.63 % (855632)------------------------------
% 71.10/10.63 % (855632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855632)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855632)Termination reason: Instruction limit
% 71.10/10.63 % (855632)Termination phase: Saturation
% 71.10/10.63 % (855632)Time elapsed: 0.456 s
% 71.10/10.63 % (855632)Peak memory usage: 57 MB
% 71.10/10.63 % (855632)Instructions burned: 881 (million)
% 71.10/10.63 % (855638)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=720859703:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 71.10/10.63 % (855640)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2962944615:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 71.10/10.63 % (855638)Instruction limit reached!
% 71.10/10.63 % (855638)------------------------------
% 71.10/10.63 % (855638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855638)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855638)Termination reason: Instruction limit
% 71.10/10.63 % (855638)Termination phase: Property scanning
% 71.10/10.63 % (855638)Time elapsed: 0.482 s
% 71.10/10.63 % (855638)Peak memory usage: 71 MB
% 71.10/10.63 % (855638)Instructions burned: 920 (million)
% 71.10/10.63 % (855649)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3065865252:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 71.10/10.63 % (855649)Instruction limit reached!
% 71.10/10.63 % (855649)------------------------------
% 71.10/10.63 % (855649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855649)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855649)Termination reason: Instruction limit
% 71.10/10.63 % (855649)Termination phase: Saturation
% 71.10/10.63 % (855649)Time elapsed: 1.427 s
% 71.10/10.63 % (855649)Peak memory usage: 59 MB
% 71.10/10.63 % (855649)Instructions burned: 1472 (million)
% 71.10/10.63 % (855682)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2463200382:i=6324_2964 on theBenchmark for (2964ds/6324Mi)
% 71.10/10.63 % Detected minimum model sizes of [447]
% 71.10/10.63 % Detected maximum model sizes of [max]
% 71.10/10.63 % (855636)Cannot represent all propositional literals internally
% 71.10/10.63 % (855636)Refutation not found, incomplete strategy
% 71.10/10.63 % (855636)------------------------------
% 71.10/10.63 % (855636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.10/10.63 % (855636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.10/10.63 % (855636)CaDiCaL version: 2.1.3
% 71.10/10.63 % (855636)Termination reason: Refutation not found, incomplete strategy
% 71.10/10.63 % (855636)Time elapsed: 2.416 s
% 71.10/10.63 % (855636)Peak memory usage: 137 MB
% 92.35/13.75 % (855636)Instructions burned: 5331 (million)
% 92.35/13.75 % (855636)------------------------------
% 92.35/13.75 % (855636)------------------------------
% 92.35/13.75 % (855684)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4004253747:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 92.35/13.75 % Detected minimum model sizes of [447]
% 92.35/13.75 % Detected maximum model sizes of [max]
% 92.35/13.75 % (855565)Cannot represent all propositional literals internally
% 92.35/13.75 % (855565)Refutation not found, incomplete strategy
% 92.35/13.75 % (855565)------------------------------
% 92.35/13.75 % (855565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.35/13.75 % (855565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.35/13.75 % (855565)CaDiCaL version: 2.1.3
% 92.35/13.75 % (855565)Termination reason: Refutation not found, incomplete strategy
% 92.35/13.75 % (855565)Time elapsed: 3.754 s
% 92.35/13.75 % (855565)Peak memory usage: 148 MB
% 92.35/13.75 % (855565)Instructions burned: 5908 (million)
% 92.35/13.75 % (855565)------------------------------
% 92.35/13.75 % (855565)------------------------------
% 92.35/13.75 % (855689)ott-2_1_sil=16000:newcnf=on:random_seed=2031189474:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 92.35/13.75 % Detected minimum model sizes of [447]
% 92.35/13.75 % Detected maximum model sizes of [max]
% 92.35/13.75 % (855634)Cannot represent all propositional literals internally
% 92.35/13.75 % (855634)Refutation not found, incomplete strategy
% 92.35/13.75 % (855634)------------------------------
% 92.35/13.75 % (855634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.35/13.75 % (855634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.35/13.75 % (855634)CaDiCaL version: 2.1.3
% 92.35/13.75 % (855634)Termination reason: Refutation not found, incomplete strategy
% 92.35/13.75 % (855634)Time elapsed: 3.632 s
% 92.35/13.75 % (855634)Peak memory usage: 132 MB
% 92.35/13.75 % (855634)Instructions burned: 5132 (million)
% 92.35/13.75 % (855684)Instruction limit reached!
% 92.35/13.75 % (855684)------------------------------
% 92.35/13.75 % (855684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.35/13.75 % (855684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.35/13.75 % (855634)------------------------------
% 92.35/13.75 % (855634)------------------------------
% 92.35/13.75 % (855684)CaDiCaL version: 2.1.3
% 92.35/13.75 % (855684)Termination reason: Instruction limit
% 92.35/13.75 % (855684)Termination phase: Finite model building preprocessing
% 92.35/13.75 % (855684)Time elapsed: 1.082 s
% 92.35/13.75 % (855684)Peak memory usage: 104 MB
% 92.35/13.75 % (855684)Instructions burned: 2175 (million)
% 92.35/13.75 % (855689)Instruction limit reached!
% 92.35/13.75 % (855689)------------------------------
% 92.35/13.75 % (855689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.35/13.75 % (855689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.35/13.75 % (855689)CaDiCaL version: 2.1.3
% 92.35/13.75 % (855689)Termination reason: Instruction limit
% 92.35/13.75 % (855689)Termination phase: Saturation
% 92.35/13.75 % (855689)Time elapsed: 0.721 s
% 92.35/13.75 % (855689)Peak memory usage: 50 MB
% 92.35/13.75 % (855689)Instructions burned: 869 (million)
% 92.35/13.75 % (855696)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3409268644:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 92.35/13.75 % (855695)ott+10_1_sil=32000:tgt=ground:random_seed=2842725483:i=5114:av=off_2949 on theBenchmark for (2949ds/5114Mi)
% 92.35/13.75 % (855697)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4283291:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 92.35/13.75 % (855640)Instruction limit reached!
% 92.35/13.75 % (855640)------------------------------
% 92.35/13.75 % (855640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.35/13.75 % (855640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.35/13.75 % (855640)CaDiCaL version: 2.1.3
% 92.35/13.75 % (855640)Termination reason: Instruction limit
% 92.35/13.75 % (855640)Termination phase: Saturation
% 92.35/13.75 % (855640)Time elapsed: 4.327 s
% 92.35/13.75 % (855640)Peak memory usage: 95 MB
% 92.35/13.75 % (855640)Instructions burned: 5131 (million)
% 92.35/13.75 % (855709)dis+21_1_sil=32000:sas=cadical:random_seed=3163027686:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 92.35/13.75 % (855697)Instruction limit reached!
% 92.35/13.75 % (855697)------------------------------
% 92.35/13.75 % (855697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855697)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855697)Termination reason: Instruction limit
% 76.77/18.98 % (855697)Termination phase: Saturation
% 76.77/18.98 % (855697)Time elapsed: 2.136 s
% 76.77/18.98 % (855697)Peak memory usage: 107 MB
% 76.77/18.98 % (855697)Instructions burned: 3513 (million)
% 76.77/18.98 % (855716)ott+11_1_sil=16000:gs=on:random_seed=3152179731:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi)
% 76.77/18.98 % (855716)Instruction limit reached!
% 76.77/18.98 % (855716)------------------------------
% 76.77/18.98 % (855716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855716)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855716)Termination reason: Instruction limit
% 76.77/18.98 % (855716)Termination phase: Saturation
% 76.77/18.98 % (855716)Time elapsed: 1.309 s
% 76.77/18.98 % (855716)Peak memory usage: 92 MB
% 76.77/18.98 % (855716)Instructions burned: 2252 (million)
% 76.77/18.98 % (855720)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3713359027:fmbsr=1.6:i=67534_2914 on theBenchmark for (2914ds/67534Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855682)Cannot represent all propositional literals internally
% 76.77/18.98 % (855682)Refutation not found, incomplete strategy
% 76.77/18.98 % (855682)------------------------------
% 76.77/18.98 % (855682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855682)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855682)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855682)Time elapsed: 5.242 s
% 76.77/18.98 % (855682)Peak memory usage: 147 MB
% 76.77/18.98 % (855682)Instructions burned: 5895 (million)
% 76.77/18.98 % (855682)------------------------------
% 76.77/18.98 % (855682)------------------------------
% 76.77/18.98 % (855723)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=639055049:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2910 on theBenchmark for (2910ds/4591Mi)
% 76.77/18.98 % (855709)Instruction limit reached!
% 76.77/18.98 % (855709)------------------------------
% 76.77/18.98 % (855709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855709)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855709)Termination reason: Instruction limit
% 76.77/18.98 % (855709)Termination phase: Saturation
% 76.77/18.98 % (855709)Time elapsed: 3.019 s
% 76.77/18.98 % (855709)Peak memory usage: 67 MB
% 76.77/18.98 % (855709)Instructions burned: 3773 (million)
% 76.77/18.98 % (855725)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=654688432:i=29340_2909 on theBenchmark for (2909ds/29340Mi)
% 76.77/18.98 % (855695)Instruction limit reached!
% 76.77/18.98 % (855695)------------------------------
% 76.77/18.98 % (855695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855695)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855695)Termination reason: Instruction limit
% 76.77/18.98 % (855695)Termination phase: Saturation
% 76.77/18.98 % (855695)Time elapsed: 5.149 s
% 76.77/18.98 % (855695)Peak memory usage: 76 MB
% 76.77/18.98 % (855695)Instructions burned: 5114 (million)
% 76.77/18.98 % (855732)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2584726502:i=5211_2897 on theBenchmark for (2897ds/5211Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855696)Cannot represent all propositional literals internally
% 76.77/18.98 % (855696)Refutation not found, incomplete strategy
% 76.77/18.98 % (855696)------------------------------
% 76.77/18.98 % (855696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855696)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855696)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855696)Time elapsed: 5.295 s
% 76.77/18.98 % (855696)Peak memory usage: 149 MB
% 76.77/18.98 % (855696)Instructions burned: 5906 (million)
% 76.77/18.98 % (855696)------------------------------
% 76.77/18.98 % (855696)------------------------------
% 76.77/18.98 % (855734)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2138100986:i=5497:nm=2_2895 on theBenchmark for (2895ds/5497Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855720)Cannot represent all propositional literals internally
% 76.77/18.98 % (855720)Refutation not found, incomplete strategy
% 76.77/18.98 % (855720)------------------------------
% 76.77/18.98 % (855720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855720)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855720)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855720)Time elapsed: 2.725 s
% 76.77/18.98 % (855720)Peak memory usage: 141 MB
% 76.77/18.98 % (855720)Instructions burned: 5906 (million)
% 76.77/18.98 % (855720)------------------------------
% 76.77/18.98 % (855720)------------------------------
% 76.77/18.98 % (855736)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2688370598:fmbsr=2:i=46332_2886 on theBenchmark for (2886ds/46332Mi)
% 76.77/18.98 % (855723)Instruction limit reached!
% 76.77/18.98 % (855723)------------------------------
% 76.77/18.98 % (855723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855723)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855723)Termination reason: Instruction limit
% 76.77/18.98 % (855723)Termination phase: Saturation
% 76.77/18.98 % (855723)Time elapsed: 3.326 s
% 76.77/18.98 % (855723)Peak memory usage: 70 MB
% 76.77/18.98 % (855723)Instructions burned: 4592 (million)
% 76.77/18.98 % (855891)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3711981403:i=14071_2876 on theBenchmark for (2876ds/14071Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855736)Cannot represent all propositional literals internally
% 76.77/18.98 % (855736)Refutation not found, incomplete strategy
% 76.77/18.98 % (855736)------------------------------
% 76.77/18.98 % (855736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855736)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855736)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855736)Time elapsed: 1.477 s
% 76.77/18.98 % (855736)Peak memory usage: 141 MB
% 76.77/18.98 % (855736)Instructions burned: 5906 (million)
% 76.77/18.98 % (855736)------------------------------
% 76.77/18.98 % (855736)------------------------------
% 76.77/18.98 % (855893)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4081762928:i=22565:add=on:rawr=on_2871 on theBenchmark for (2871ds/22565Mi)
% 76.77/18.98 % (855732)Instruction limit reached!
% 76.77/18.98 % (855732)------------------------------
% 76.77/18.98 % (855732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855732)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855732)Termination reason: Instruction limit
% 76.77/18.98 % (855732)Termination phase: Saturation
% 76.77/18.98 % (855732)Time elapsed: 2.821 s
% 76.77/18.98 % (855732)Peak memory usage: 70 MB
% 76.77/18.98 % (855732)Instructions burned: 5212 (million)
% 76.77/18.98 % (855895)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2081562364:i=8173:av=off_2868 on theBenchmark for (2868ds/8173Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855734)Cannot represent all propositional literals internally
% 76.77/18.98 % (855734)Refutation not found, incomplete strategy
% 76.77/18.98 % (855734)------------------------------
% 76.77/18.98 % (855734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855734)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855734)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855734)Time elapsed: 2.994 s
% 76.77/18.98 % (855734)Peak memory usage: 141 MB
% 76.77/18.98 % (855734)Instructions burned: 5487 (million)
% 76.77/18.98 % (855734)------------------------------
% 76.77/18.98 % (855734)------------------------------
% 76.77/18.98 % (855897)dis+10_16:1_sil=16000:random_seed=3844210947:i=9155:fsr=off_2865 on theBenchmark for (2865ds/9155Mi)
% 76.77/18.98 % Detected minimum model sizes of [447]
% 76.77/18.98 % Detected maximum model sizes of [max]
% 76.77/18.98 % (855891)Cannot represent all propositional literals internally
% 76.77/18.98 % (855891)Refutation not found, incomplete strategy
% 76.77/18.98 % (855891)------------------------------
% 76.77/18.98 % (855891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855891)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855891)Termination reason: Refutation not found, incomplete strategy
% 76.77/18.98 % (855891)Time elapsed: 2.603 s
% 76.77/18.98 % (855891)Peak memory usage: 139 MB
% 76.77/18.98 % (855891)Instructions burned: 5457 (million)
% 76.77/18.98 % (855891)------------------------------
% 76.77/18.98 % (855891)------------------------------
% 76.77/18.98 % (856186)ott-3_8_sil=64000:random_seed=1102177745:i=20139:bs=on_2850 on theBenchmark for (2850ds/20139Mi)
% 76.77/18.98 % (855897)Instruction limit reached!
% 76.77/18.98 % (855897)------------------------------
% 76.77/18.98 % (855897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855897)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855897)Termination reason: Instruction limit
% 76.77/18.98 % (855897)Termination phase: Saturation
% 76.77/18.98 % (855897)Time elapsed: 4.673 s
% 76.77/18.98 % (855897)Peak memory usage: 130 MB
% 76.77/18.98 % (855897)Instructions burned: 9157 (million)
% 76.77/18.98 % (856188)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3899184779:fmbsr=2:i=32576_2817 on theBenchmark for (2817ds/32576Mi)
% 76.77/18.98 % (855895)Instruction limit reached!
% 76.77/18.98 % (855895)------------------------------
% 76.77/18.98 % (855895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/18.98 % (855895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/18.98 % (855895)CaDiCaL version: 2.1.3
% 76.77/18.98 % (855895)Termination reason: Instruction limit
% 76.77/18.98 % (855895)Termination phase: Saturation
% 76.77/18.98 % (855895)Time elapsed: 5.110 s
% 76.77/18.98 % (855895)Peak memory usage: 93 MB
% 76.77/18.98 % (855895)Instructions burned: 8173 (million)
% 76.77/18.98 % (856190)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3503960352:i=11404_2817 on theBenchmark for (2817ds/11404Mi)
% 76.77/18.98 % (856186) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-855464-856186"...
% 76.77/18.98 % (856186)...printing done.
% 76.77/18.98 % (856186)Refutation found. Thanks to Tanya!
% 76.77/18.98 % SZS status Theorem for theBenchmark
% 76.77/18.98 % SZS output start Proof for theBenchmark
% See solution above
% 76.77/19.01 % (856186)------------------------------
% 76.77/19.01 % (856186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.77/19.01 % (856186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.77/19.01 % (856186)CaDiCaL version: 2.1.3
% 76.77/19.01 % (856186)Termination reason: Refutation
% 76.77/19.01 % (856186)Time elapsed: 3.562 s
% 76.77/19.01 % (856186)Peak memory usage: 78 MB
% 76.77/19.01 % (856186)Instructions burned: 6021 (million)
% 76.77/19.01 % (855464)Success in time 18.748 s
% 76.77/19.01 % Vampire exiting
%------------------------------------------------------------------------------