%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR090+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:08 AM UTC 2026
% Result : Theorem 50.52s 17.20s
% Output : Refutation 118.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 15
% Syntax : Number of formulae : 74 ( 25 unt; 4 def)
% Number of atoms : 193 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 234 ( 115 ~; 103 |; 7 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 45 ( 0 sgn 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.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/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f905,axiom,
s__subclass(s__TimeInterval,s__TimePosition),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_908) ).
fof(f1259,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__TimePosition)
& s__instance(X1,s__TimePosition)
& s__instance(X0,s__TimePosition) )
=> ( ( s__temporalPart(X0,X1)
& s__temporalPart(X1,X2) )
=> s__temporalPart(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1262) ).
fof(f12291,axiom,
s__subclass(s__Day,s__TimePosition),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+3.ax',kb_SUMOcache_5074) ).
fof(f14788,axiom,
s__instance(s__Time17_1,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f14789,axiom,
s__instance(s__Time17_2,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f14790,axiom,
s__instance(s__Time17_3,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f14791,axiom,
s__temporalPart(s__Time17_1,s__Time17_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(f14792,axiom,
s__temporalPart(s__Time17_2,s__Time17_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(f14793,conjecture,
s__temporalPart(s__Time17_1,s__Time17_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f14794,negated_conjecture,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(negated_conjecture,[status(cth)],[f14793]) ).
fof(f14798,plain,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(flattening,[],[f14794]) ).
fof(f14889,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f14890,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(f14891,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,[],[f14890]) ).
fof(f16049,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(ennf_transformation,[],[f1259]) ).
fof(f16050,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(flattening,[],[f16049]) ).
fof(f21908,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f14889]) ).
fof(f21909,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f14889]) ).
fof(f21910,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,[],[f14891]) ).
fof(f22869,plain,
s__subclass(s__TimeInterval,s__TimePosition),
inference(cnf_transformation,[],[f905]) ).
fof(f23295,plain,
! [X2,X0,X1] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(cnf_transformation,[],[f16050]) ).
fof(f35203,plain,
s__subclass(s__Day,s__TimePosition),
inference(cnf_transformation,[],[f12291]) ).
fof(f37700,plain,
s__instance(s__Time17_1,s__TimeInterval),
inference(cnf_transformation,[],[f14788]) ).
fof(f37701,plain,
s__instance(s__Time17_2,s__TimeInterval),
inference(cnf_transformation,[],[f14789]) ).
fof(f37702,plain,
s__instance(s__Time17_3,s__TimeInterval),
inference(cnf_transformation,[],[f14790]) ).
fof(f37703,plain,
s__temporalPart(s__Time17_1,s__Time17_2),
inference(cnf_transformation,[],[f14791]) ).
fof(f37704,plain,
s__temporalPart(s__Time17_2,s__Time17_3),
inference(cnf_transformation,[],[f14792]) ).
fof(f37705,plain,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(cnf_transformation,[],[f14798]) ).
fof(f45068,definition,
( spl504_83
<=> s__instance(s__TimePosition,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[spl504_83])],[avatar_definition]) ).
fof(f45069,plain,
( s__instance(s__TimePosition,s__SetOrClass)
| ~ spl504_83 ),
inference(avatar_component_clause,[],[f45068]) ).
fof(f45070,plain,
( ~ s__instance(s__TimePosition,s__SetOrClass)
| spl504_83 ),
inference(avatar_component_clause,[],[f45068]) ).
fof(f45077,plain,
( ! [X0] : ~ s__subclass(X0,s__TimePosition)
| spl504_83 ),
inference(resolution,[],[f45070,f21908]) ).
fof(f45086,plain,
( $false
| spl504_83 ),
inference(resolution,[],[f45077,f35203]) ).
fof(f45143,plain,
spl504_83,
inference(avatar_contradiction_clause,[],[f45086]) ).
fof(f134869,plain,
! [X0] :
( ~ s__temporalPart(s__Time17_1,X0)
| ~ s__temporalPart(X0,s__Time17_3)
| ~ s__instance(s__Time17_3,s__TimePosition)
| ~ s__instance(X0,s__TimePosition)
| ~ s__instance(s__Time17_1,s__TimePosition) ),
inference(resolution,[],[f23295,f37705]) ).
fof(f134881,definition,
( spl504_726
<=> s__instance(s__Time17_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_726])],[avatar_definition]) ).
fof(f134883,plain,
( ~ s__instance(s__Time17_1,s__TimePosition)
| spl504_726 ),
inference(avatar_component_clause,[],[f134881]) ).
fof(f134885,definition,
( spl504_727
<=> s__instance(s__Time17_3,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl504_727])],[avatar_definition]) ).
fof(f134887,plain,
( ~ s__instance(s__Time17_3,s__TimePosition)
| spl504_727 ),
inference(avatar_component_clause,[],[f134885]) ).
fof(f134889,definition,
( spl504_728
<=> ! [X0] :
( ~ s__temporalPart(s__Time17_1,X0)
| ~ s__instance(X0,s__TimePosition)
| ~ s__temporalPart(X0,s__Time17_3) ) ),
introduced(definition,[new_symbols(definition,[spl504_728])],[avatar_definition]) ).
fof(f134890,plain,
( ! [X0] :
( ~ s__temporalPart(s__Time17_1,X0)
| ~ s__temporalPart(X0,s__Time17_3)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl504_728 ),
inference(avatar_component_clause,[],[f134889]) ).
fof(f134891,plain,
( ~ spl504_726
| ~ spl504_727
| spl504_728 ),
inference(avatar_split_clause,[],[f134869,f134889,f134885,f134881]) ).
fof(f134909,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_1,X0)
| ~ s__instance(s__TimePosition,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_726 ),
inference(resolution,[],[f134883,f21910]) ).
fof(f134910,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_83
| spl504_726 ),
inference(forward_subsumption_resolution,[],[f134909,f45069]) ).
fof(f134913,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_1,X0) )
| ~ spl504_83
| spl504_726 ),
inference(forward_subsumption_resolution,[],[f134910,f21909]) ).
fof(f134931,plain,
( ~ s__instance(s__Time17_1,s__TimeInterval)
| ~ spl504_83
| spl504_726 ),
inference(resolution,[],[f134913,f22869]) ).
fof(f134958,plain,
( $false
| ~ spl504_83
| spl504_726 ),
inference(forward_subsumption_resolution,[],[f134931,f37700]) ).
fof(f134959,plain,
( ~ spl504_83
| spl504_726 ),
inference(avatar_contradiction_clause,[],[f134958]) ).
fof(f135031,plain,
( ~ s__temporalPart(s__Time17_1,s__Time17_2)
| ~ s__instance(s__Time17_2,s__TimePosition)
| ~ spl504_728 ),
inference(resolution,[],[f134890,f37704]) ).
fof(f135042,plain,
( ~ s__instance(s__Time17_2,s__TimePosition)
| ~ spl504_728 ),
inference(forward_subsumption_resolution,[],[f135031,f37703]) ).
fof(f135055,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_2,X0)
| ~ s__instance(s__TimePosition,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_728 ),
inference(resolution,[],[f135042,f21910]) ).
fof(f135056,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_2,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_83
| ~ spl504_728 ),
inference(forward_subsumption_resolution,[],[f135055,f45069]) ).
fof(f135059,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_2,X0) )
| ~ spl504_83
| ~ spl504_728 ),
inference(forward_subsumption_resolution,[],[f135056,f21909]) ).
fof(f135079,plain,
( ~ s__instance(s__Time17_2,s__TimeInterval)
| ~ spl504_83
| ~ spl504_728 ),
inference(resolution,[],[f135059,f22869]) ).
fof(f135106,plain,
( $false
| ~ spl504_83
| ~ spl504_728 ),
inference(forward_subsumption_resolution,[],[f135079,f37701]) ).
fof(f135107,plain,
( ~ spl504_83
| ~ spl504_728 ),
inference(avatar_contradiction_clause,[],[f135106]) ).
fof(f135117,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_3,X0)
| ~ s__instance(s__TimePosition,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl504_727 ),
inference(resolution,[],[f134887,f21910]) ).
fof(f135118,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_3,X0)
| ~ s__instance(X0,s__SetOrClass) )
| ~ spl504_83
| spl504_727 ),
inference(forward_subsumption_resolution,[],[f135117,f45069]) ).
fof(f135121,plain,
( ! [X0] :
( ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_3,X0) )
| ~ spl504_83
| spl504_727 ),
inference(forward_subsumption_resolution,[],[f135118,f21909]) ).
fof(f135149,plain,
( ~ s__instance(s__Time17_3,s__TimeInterval)
| ~ spl504_83
| spl504_727 ),
inference(resolution,[],[f135121,f22869]) ).
fof(f135176,plain,
( $false
| ~ spl504_83
| spl504_727 ),
inference(forward_subsumption_resolution,[],[f135149,f37702]) ).
fof(f135177,plain,
( ~ spl504_83
| spl504_727 ),
inference(avatar_contradiction_clause,[],[f135176]) ).
cnf(s334,plain,
spl504_83,
inference(sat_conversion,[],[f45143]) ).
cnf(s2660,plain,
( ~ spl504_726
| ~ spl504_727
| spl504_728 ),
inference(sat_conversion,[],[f134891]) ).
cnf(s2661,plain,
( ~ spl504_83
| spl504_726 ),
inference(sat_conversion,[],[f134959]) ).
cnf(s2662,plain,
( ~ spl504_83
| ~ spl504_728 ),
inference(sat_conversion,[],[f135107]) ).
cnf(s2663,plain,
( ~ spl504_83
| spl504_727 ),
inference(sat_conversion,[],[f135177]) ).
cnf(s2733,plain,
spl504_727,
inference(rat,[],[s2663,s334]) ).
cnf(s2734,plain,
~ spl504_728,
inference(rat,[],[s2662,s334]) ).
cnf(s2735,plain,
spl504_726,
inference(rat,[],[s2661,s334]) ).
cnf(s2736,plain,
$false,
inference(rat,[],[s2660,s2734,s2733,s2735]) ).
fof(f135178,plain,
$false,
inference(avatar_sat_refutation,[],[s2736]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR090+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n010.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:40:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.30/2.03 % (2442011)Will run a generic schedule for satisfiability detection.
% 8.30/2.03 % (2442017)% WARNING: option uhcvi not known.
% 8.30/2.03 % (2442017)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1716120208:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 8.30/2.03 % (2442016)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2563847462_2997 on theBenchmark for (2997ds/0Mi)
% 8.30/2.03 % (2442018)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2187999801:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 8.30/2.03 % (2442019)dis+10_1_sil=32000:sp=arity:random_seed=832959782:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 8.30/2.03 % (2442021)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1382721160:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 8.30/2.03 % (2442020)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1639460612:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 8.30/2.03 % (2442022)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3682967457:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 8.30/2.03 % (2442019)Instruction limit reached!
% 8.30/2.03 % (2442019)------------------------------
% 8.30/2.03 % (2442019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/2.03 % (2442019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/2.03 % (2442019)CaDiCaL version: 2.1.3
% 8.30/2.03 % (2442019)Termination reason: Instruction limit
% 8.30/2.03 % (2442019)Termination phase: Preprocessing 3
% 8.30/2.03 % (2442019)Time elapsed: 0.066 s
% 8.30/2.03 % (2442019)Peak memory usage: 29 MB
% 8.30/2.03 % (2442019)Instructions burned: 104 (million)
% 8.30/2.03 % (2442021)Instruction limit reached!
% 8.30/2.03 % (2442021)------------------------------
% 8.30/2.03 % (2442021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/2.03 % (2442021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/2.03 % (2442021)CaDiCaL version: 2.1.3
% 8.30/2.03 % (2442021)Termination reason: Instruction limit
% 8.30/2.03 % (2442021)Termination phase: Clausification
% 8.30/2.03 % (2442021)Time elapsed: 0.076 s
% 8.30/2.03 % (2442021)Peak memory usage: 31 MB
% 8.30/2.03 % (2442021)Instructions burned: 132 (million)
% 8.30/2.03 % (2442020)Instruction limit reached!
% 8.30/2.03 % (2442020)------------------------------
% 8.30/2.03 % (2442020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/2.03 % (2442020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/2.03 % (2442020)CaDiCaL version: 2.1.3
% 8.30/2.03 % (2442020)Termination reason: Instruction limit
% 8.30/2.03 % (2442020)Termination phase: NewCNF
% 8.30/2.03 % (2442020)Time elapsed: 0.077 s
% 8.30/2.03 % (2442020)Peak memory usage: 32 MB
% 8.30/2.03 % (2442020)Instructions burned: 116 (million)
% 8.30/2.03 % (2442030)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=827220833:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 8.30/2.03 % (2442031)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3411494710:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 8.30/2.03 % (2442032)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=2188030543:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 8.30/2.03 % (2442022)Instruction limit reached!
% 8.30/2.03 % (2442022)------------------------------
% 8.30/2.03 % (2442022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/2.03 % (2442022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.30/2.03 % (2442022)CaDiCaL version: 2.1.3
% 8.30/2.03 % (2442022)Termination reason: Instruction limit
% 8.30/2.03 % (2442022)Termination phase: Property scanning
% 8.30/2.03 % (2442022)Time elapsed: 0.104 s
% 8.30/2.03 % (2442022)Peak memory usage: 31 MB
% 8.30/2.03 % (2442022)Instructions burned: 160 (million)
% 8.30/2.03 % (2442036)ott-21_1_sil=16000:fs=off:random_seed=1386271429:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 8.30/2.03 % (2442031)Instruction limit reached!
% 8.30/2.03 % (2442031)------------------------------
% 8.30/2.03 % (2442031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.30/2.03 % (2442031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442031)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442031)Termination reason: Instruction limit
% 18.37/3.13 % (2442031)Termination phase: Clausification
% 18.37/3.13 % (2442031)Time elapsed: 0.075 s
% 18.37/3.13 % (2442031)Peak memory usage: 31 MB
% 18.37/3.13 % (2442031)Instructions burned: 131 (million)
% 18.37/3.13 % (2442038)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2737626376:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 18.37/3.13 % (2442036)Instruction limit reached!
% 18.37/3.13 % (2442036)------------------------------
% 18.37/3.13 % (2442036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442036)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442036)Termination reason: Instruction limit
% 18.37/3.13 % (2442036)Termination phase: Property scanning
% 18.37/3.13 % (2442036)Time elapsed: 0.103 s
% 18.37/3.13 % (2442036)Peak memory usage: 31 MB
% 18.37/3.13 % (2442036)Instructions burned: 181 (million)
% 18.37/3.13 % (2442040)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=705008246:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 18.37/3.13 % (2442038)Instruction limit reached!
% 18.37/3.13 % (2442038)------------------------------
% 18.37/3.13 % (2442038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442038)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442038)Termination reason: Instruction limit
% 18.37/3.13 % (2442038)Termination phase: Saturation
% 18.37/3.13 % (2442038)Time elapsed: 0.230 s
% 18.37/3.13 % (2442038)Peak memory usage: 35 MB
% 18.37/3.13 % (2442038)Instructions burned: 477 (million)
% 18.37/3.13 % (2442030)Instruction limit reached!
% 18.37/3.13 % (2442030)------------------------------
% 18.37/3.13 % (2442030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442030)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442030)Termination reason: Instruction limit
% 18.37/3.13 % (2442030)Termination phase: Finite model building preprocessing
% 18.37/3.13 % (2442030)Time elapsed: 0.348 s
% 18.37/3.13 % (2442030)Peak memory usage: 42 MB
% 18.37/3.13 % (2442030)Instructions burned: 714 (million)
% 18.37/3.13 % (2442032)Instruction limit reached!
% 18.37/3.13 % (2442032)------------------------------
% 18.37/3.13 % (2442032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442032)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442032)Termination reason: Instruction limit
% 18.37/3.13 % (2442032)Termination phase: Saturation
% 18.37/3.13 % (2442032)Time elapsed: 0.339 s
% 18.37/3.13 % (2442032)Peak memory usage: 38 MB
% 18.37/3.13 % (2442032)Instructions burned: 685 (million)
% 18.37/3.13 % (2442042)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3032341100:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 18.37/3.13 % (2442043)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2457302526:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 18.37/3.13 % (2442044)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=2685829021:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 18.37/3.13 % (2442040)Instruction limit reached!
% 18.37/3.13 % (2442040)------------------------------
% 18.37/3.13 % (2442040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.37/3.13 % (2442040)CaDiCaL version: 2.1.3
% 18.37/3.13 % (2442040)Termination reason: Instruction limit
% 18.37/3.13 % (2442040)Termination phase: Finite model building preprocessing
% 18.37/3.13 % (2442040)Time elapsed: 0.418 s
% 18.37/3.13 % (2442040)Peak memory usage: 46 MB
% 18.37/3.13 % (2442040)Instructions burned: 865 (million)
% 18.37/3.13 % (2442048)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1231540268:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 18.37/3.13 % (2442044)Instruction limit reached!
% 18.37/3.13 % (2442044)------------------------------
% 18.37/3.13 % (2442044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.37/3.13 % (2442044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442044)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442044)Termination reason: Instruction limit
% 32.57/5.04 % (2442044)Termination phase: Saturation
% 32.57/5.04 % (2442044)Time elapsed: 0.346 s
% 32.57/5.04 % (2442044)Peak memory usage: 43 MB
% 32.57/5.04 % (2442044)Instructions burned: 693 (million)
% 32.57/5.04 % (2442050)fmb+10_1_sil=64000:random_seed=2953938414:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 32.57/5.04 % (2442043)Instruction limit reached!
% 32.57/5.04 % (2442043)------------------------------
% 32.57/5.04 % (2442043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.57/5.04 % (2442043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442043)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442043)Termination reason: Instruction limit
% 32.57/5.04 % (2442043)Termination phase: Finite model building preprocessing
% 32.57/5.04 % (2442043)Time elapsed: 0.429 s
% 32.57/5.04 % (2442043)Peak memory usage: 47 MB
% 32.57/5.04 % (2442043)Instructions burned: 889 (million)
% 32.57/5.04 % Detected minimum model sizes of [51]
% 32.57/5.04 % Detected maximum model sizes of [max]
% 32.57/5.04 % (2442016)Cannot represent all propositional literals internally
% 32.57/5.04 % (2442016)Refutation not found, incomplete strategy
% 32.57/5.04 % (2442016)------------------------------
% 32.57/5.04 % (2442016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.57/5.04 % (2442016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442016)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442016)Termination reason: Refutation not found, incomplete strategy
% 32.57/5.04 % (2442016)Time elapsed: 0.906 s
% 32.57/5.04 % (2442016)Peak memory usage: 61 MB
% 32.57/5.04 % (2442016)Instructions burned: 1884 (million)
% 32.57/5.04 % (2442052)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2524824288:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 32.57/5.04 % (2442016)------------------------------
% 32.57/5.04 % (2442016)------------------------------
% 32.57/5.04 % (2442054)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=592985047:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 32.57/5.04 % (2442042)Instruction limit reached!
% 32.57/5.04 % (2442042)------------------------------
% 32.57/5.04 % (2442042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.57/5.04 % (2442042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442042)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442042)Termination reason: Instruction limit
% 32.57/5.04 % (2442042)Termination phase: Saturation
% 32.57/5.04 % (2442042)Time elapsed: 0.605 s
% 32.57/5.04 % (2442042)Peak memory usage: 44 MB
% 32.57/5.04 % (2442042)Instructions burned: 1180 (million)
% 32.57/5.04 % (2442056)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2898441216:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 32.57/5.04 % (2442048)Instruction limit reached!
% 32.57/5.04 % (2442048)------------------------------
% 32.57/5.04 % (2442048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.57/5.04 % (2442048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442048)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442048)Termination reason: Instruction limit
% 32.57/5.04 % (2442048)Termination phase: Saturation
% 32.57/5.04 % (2442048)Time elapsed: 0.436 s
% 32.57/5.04 % (2442048)Peak memory usage: 45 MB
% 32.57/5.04 % (2442048)Instructions burned: 879 (million)
% 32.57/5.04 % (2442058)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1350241323:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 32.57/5.04 % (2442054)Instruction limit reached!
% 32.57/5.04 % (2442054)------------------------------
% 32.57/5.04 % (2442054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.57/5.04 % (2442054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.57/5.04 % (2442054)CaDiCaL version: 2.1.3
% 32.57/5.04 % (2442054)Termination reason: Instruction limit
% 32.57/5.04 % (2442054)Termination phase: Finite model building preprocessing
% 32.57/5.04 % (2442054)Time elapsed: 0.447 s
% 32.57/5.04 % (2442054)Peak memory usage: 47 MB
% 32.57/5.04 % (2442054)Instructions burned: 920 (million)
% 32.57/5.04 % (2442060)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3187525087:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 32.57/5.04 % Detected minimum model sizes of [51]
% 32.57/5.04 % Detected maximum model sizes of [max]
% 32.57/5.04 % (2442050)Cannot represent all propositional literals internally
% 43.67/6.69 % (2442050)Refutation not found, incomplete strategy
% 43.67/6.69 % (2442050)------------------------------
% 43.67/6.69 % (2442050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/6.69 % (2442050)CaDiCaL version: 2.1.3
% 43.67/6.69 % (2442050)Termination reason: Refutation not found, incomplete strategy
% 43.67/6.69 % (2442050)Time elapsed: 0.676 s
% 43.67/6.69 % (2442050)Peak memory usage: 51 MB
% 43.67/6.69 % (2442050)Instructions burned: 1452 (million)
% 43.67/6.69 % (2442050)------------------------------
% 43.67/6.69 % (2442050)------------------------------
% 43.67/6.69 % (2442062)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4275612568:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 43.67/6.69 % Detected minimum model sizes of [51]
% 43.67/6.69 % Detected maximum model sizes of [max]
% 43.67/6.69 % (2442052)Cannot represent all propositional literals internally
% 43.67/6.69 % (2442052)Refutation not found, incomplete strategy
% 43.67/6.69 % (2442052)------------------------------
% 43.67/6.69 % (2442052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/6.69 % (2442052)CaDiCaL version: 2.1.3
% 43.67/6.69 % (2442052)Termination reason: Refutation not found, incomplete strategy
% 43.67/6.69 % (2442052)Time elapsed: 0.701 s
% 43.67/6.69 % (2442052)Peak memory usage: 52 MB
% 43.67/6.69 % (2442052)Instructions burned: 1527 (million)
% 43.67/6.69 % (2442052)------------------------------
% 43.67/6.69 % (2442052)------------------------------
% 43.67/6.69 % (2442064)ott-2_1_sil=16000:newcnf=on:random_seed=1627238919:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 43.67/6.69 % (2442058)Instruction limit reached!
% 43.67/6.69 % (2442058)------------------------------
% 43.67/6.69 % (2442058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/6.69 % (2442058)CaDiCaL version: 2.1.3
% 43.67/6.69 % (2442058)Termination reason: Instruction limit
% 43.67/6.69 % (2442058)Termination phase: Saturation
% 43.67/6.69 % (2442058)Time elapsed: 0.774 s
% 43.67/6.69 % (2442058)Peak memory usage: 49 MB
% 43.67/6.69 % (2442058)Instructions burned: 1474 (million)
% 43.67/6.69 % (2442066)ott+10_1_sil=32000:tgt=ground:random_seed=49551923:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi)
% 43.67/6.69 % (2442064)Instruction limit reached!
% 43.67/6.69 % (2442064)------------------------------
% 43.67/6.69 % (2442064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/6.69 % (2442064)CaDiCaL version: 2.1.3
% 43.67/6.69 % (2442064)Termination reason: Instruction limit
% 43.67/6.69 % (2442064)Termination phase: Saturation
% 43.67/6.69 % (2442064)Time elapsed: 0.440 s
% 43.67/6.69 % (2442064)Peak memory usage: 43 MB
% 43.67/6.69 % (2442064)Instructions burned: 869 (million)
% 43.67/6.69 % (2442068)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2689948849:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 43.67/6.69 % Detected minimum model sizes of [51]
% 43.67/6.69 % Detected maximum model sizes of [max]
% 43.67/6.69 % (2442060)Cannot represent all propositional literals internally
% 43.67/6.69 % (2442060)Refutation not found, incomplete strategy
% 43.67/6.69 % (2442060)------------------------------
% 43.67/6.69 % (2442060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/6.69 % (2442060)CaDiCaL version: 2.1.3
% 43.67/6.69 % (2442060)Termination reason: Refutation not found, incomplete strategy
% 43.67/6.69 % (2442060)Time elapsed: 0.895 s
% 43.67/6.69 % (2442060)Peak memory usage: 58 MB
% 43.67/6.69 % (2442060)Instructions burned: 1851 (million)
% 43.67/6.69 % (2442060)------------------------------
% 43.67/6.69 % (2442060)------------------------------
% 43.67/6.69 % (2442070)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1693974772:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi)
% 43.67/6.69 % (2442062)Instruction limit reached!
% 43.67/6.69 % (2442062)------------------------------
% 43.67/6.69 % (2442062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.67/6.69 % (2442062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442062)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442062)Termination reason: Instruction limit
% 50.52/17.20 % (2442062)Termination phase: Finite model building preprocessing
% 50.52/17.20 % (2442062)Time elapsed: 1.055 s
% 50.52/17.20 % (2442062)Peak memory usage: 71 MB
% 50.52/17.20 % (2442062)Instructions burned: 2175 (million)
% 50.52/17.20 % (2442072)dis+21_1_sil=32000:sas=cadical:random_seed=1161705541:i=3773:amm=off_2970 on theBenchmark for (2970ds/3773Mi)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442068)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442068)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442068)------------------------------
% 50.52/17.20 % (2442068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442068)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442068)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442068)Time elapsed: 0.902 s
% 50.52/17.20 % (2442068)Peak memory usage: 60 MB
% 50.52/17.20 % (2442068)Instructions burned: 1867 (million)
% 50.52/17.20 % (2442068)------------------------------
% 50.52/17.20 % (2442068)------------------------------
% 50.52/17.20 % (2442074)ott+11_1_sil=16000:gs=on:random_seed=3835341913:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2966 on theBenchmark for (2966ds/2251Mi)
% 50.52/17.20 % (2442056)Instruction limit reached!
% 50.52/17.20 % (2442056)------------------------------
% 50.52/17.20 % (2442056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442056)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442056)Termination reason: Instruction limit
% 50.52/17.20 % (2442056)Termination phase: Saturation
% 50.52/17.20 % (2442056)Time elapsed: 2.683 s
% 50.52/17.20 % (2442056)Peak memory usage: 65 MB
% 50.52/17.20 % (2442056)Instructions burned: 5132 (million)
% 50.52/17.20 % (2442076)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1053351176:fmbsr=1.6:i=67534_2959 on theBenchmark for (2959ds/67534Mi)
% 50.52/17.20 % (2442070)Instruction limit reached!
% 50.52/17.20 % (2442070)------------------------------
% 50.52/17.20 % (2442070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442070)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442070)Termination reason: Instruction limit
% 50.52/17.20 % (2442070)Termination phase: Saturation
% 50.52/17.20 % (2442070)Time elapsed: 1.648 s
% 50.52/17.20 % (2442070)Peak memory usage: 73 MB
% 50.52/17.20 % (2442070)Instructions burned: 3512 (million)
% 50.52/17.20 % (2442074)Instruction limit reached!
% 50.52/17.20 % (2442074)------------------------------
% 50.52/17.20 % (2442074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442074)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442074)Termination reason: Instruction limit
% 50.52/17.20 % (2442074)Termination phase: Saturation
% 50.52/17.20 % (2442074)Time elapsed: 0.952 s
% 50.52/17.20 % (2442074)Peak memory usage: 52 MB
% 50.52/17.20 % (2442074)Instructions burned: 2251 (million)
% 50.52/17.20 % (2442078)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=869738756:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2956 on theBenchmark for (2956ds/4591Mi)
% 50.52/17.20 % (2442079)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3261246221:i=29340_2956 on theBenchmark for (2956ds/29340Mi)
% 50.52/17.20 % (2442072)Instruction limit reached!
% 50.52/17.20 % (2442072)------------------------------
% 50.52/17.20 % (2442072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442072)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442072)Termination reason: Instruction limit
% 50.52/17.20 % (2442072)Termination phase: Saturation
% 50.52/17.20 % (2442072)Time elapsed: 1.848 s
% 50.52/17.20 % (2442072)Peak memory usage: 86 MB
% 50.52/17.20 % (2442072)Instructions burned: 3775 (million)
% 50.52/17.20 % (2442066)Instruction limit reached!
% 50.52/17.20 % (2442066)------------------------------
% 50.52/17.20 % (2442066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442066)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442066)Termination reason: Instruction limit
% 50.52/17.20 % (2442066)Termination phase: Saturation
% 50.52/17.20 % (2442066)Time elapsed: 2.555 s
% 50.52/17.20 % (2442066)Peak memory usage: 85 MB
% 50.52/17.20 % (2442066)Instructions burned: 5115 (million)
% 50.52/17.20 % (2442082)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3940669433:i=5211_2951 on theBenchmark for (2951ds/5211Mi)
% 50.52/17.20 % (2442084)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4259547898:i=5497:nm=2_2951 on theBenchmark for (2951ds/5497Mi)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442076)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442076)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442076)------------------------------
% 50.52/17.20 % (2442076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442076)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442076)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442076)Time elapsed: 0.754 s
% 50.52/17.20 % (2442076)Peak memory usage: 53 MB
% 50.52/17.20 % (2442076)Instructions burned: 1686 (million)
% 50.52/17.20 % (2442076)------------------------------
% 50.52/17.20 % (2442076)------------------------------
% 50.52/17.20 % (2442086)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1430133483:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442086)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442086)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442086)------------------------------
% 50.52/17.20 % (2442086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442086)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442086)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442086)Time elapsed: 0.753 s
% 50.52/17.20 % (2442086)Peak memory usage: 53 MB
% 50.52/17.20 % (2442086)Instructions burned: 1687 (million)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442084)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442084)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442084)------------------------------
% 50.52/17.20 % (2442084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442084)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442084)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442084)Time elapsed: 0.812 s
% 50.52/17.20 % (2442084)Peak memory usage: 54 MB
% 50.52/17.20 % (2442084)Instructions burned: 1715 (million)
% 50.52/17.20 % (2442086)------------------------------
% 50.52/17.20 % (2442086)------------------------------
% 50.52/17.20 % (2442084)------------------------------
% 50.52/17.20 % (2442084)------------------------------
% 50.52/17.20 % (2442088)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4156273550:i=14071_2943 on theBenchmark for (2943ds/14071Mi)
% 50.52/17.20 % (2442089)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=549540928:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442088)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442088)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442088)------------------------------
% 50.52/17.20 % (2442088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442088)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442088)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442088)Time elapsed: 0.715 s
% 50.52/17.20 % (2442088)Peak memory usage: 53 MB
% 50.52/17.20 % (2442088)Instructions burned: 1556 (million)
% 50.52/17.20 % (2442088)------------------------------
% 50.52/17.20 % (2442088)------------------------------
% 50.52/17.20 % (2442092)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1975767666:i=8173:av=off_2935 on theBenchmark for (2935ds/8173Mi)
% 50.52/17.20 % (2442078)Instruction limit reached!
% 50.52/17.20 % (2442078)------------------------------
% 50.52/17.20 % (2442078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442078)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442078)Termination reason: Instruction limit
% 50.52/17.20 % (2442078)Termination phase: Saturation
% 50.52/17.20 % (2442078)Time elapsed: 2.609 s
% 50.52/17.20 % (2442078)Peak memory usage: 98 MB
% 50.52/17.20 % (2442078)Instructions burned: 4592 (million)
% 50.52/17.20 % (2442082)Instruction limit reached!
% 50.52/17.20 % (2442082)------------------------------
% 50.52/17.20 % (2442082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442082)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442082)Termination reason: Instruction limit
% 50.52/17.20 % (2442082)Termination phase: Saturation
% 50.52/17.20 % (2442082)Time elapsed: 2.152 s
% 50.52/17.20 % (2442082)Peak memory usage: 66 MB
% 50.52/17.20 % (2442082)Instructions burned: 5214 (million)
% 50.52/17.20 % (2442094)dis+10_16:1_sil=16000:random_seed=378791911:i=9155:fsr=off_2930 on theBenchmark for (2930ds/9155Mi)
% 50.52/17.20 % (2442095)ott-3_8_sil=64000:random_seed=1309179901:i=20139:bs=on_2930 on theBenchmark for (2930ds/20139Mi)
% 50.52/17.20 % (2442092)Instruction limit reached!
% 50.52/17.20 % (2442092)------------------------------
% 50.52/17.20 % (2442092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442092)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442092)Termination reason: Instruction limit
% 50.52/17.20 % (2442092)Termination phase: Saturation
% 50.52/17.20 % (2442092)Time elapsed: 4.376 s
% 50.52/17.20 % (2442092)Peak memory usage: 113 MB
% 50.52/17.20 % (2442092)Instructions burned: 8174 (million)
% 50.52/17.20 % (2442098)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1958029425:fmbsr=2:i=32576_2891 on theBenchmark for (2891ds/32576Mi)
% 50.52/17.20 % (2442094)Instruction limit reached!
% 50.52/17.20 % (2442094)------------------------------
% 50.52/17.20 % (2442094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442094)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442094)Termination reason: Instruction limit
% 50.52/17.20 % (2442094)Termination phase: Saturation
% 50.52/17.20 % (2442094)Time elapsed: 4.554 s
% 50.52/17.20 % (2442094)Peak memory usage: 157 MB
% 50.52/17.20 % (2442094)Instructions burned: 9156 (million)
% 50.52/17.20 % (2442100)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1215254348:i=11404_2884 on theBenchmark for (2884ds/11404Mi)
% 50.52/17.20 % Detected minimum model sizes of [51]
% 50.52/17.20 % Detected maximum model sizes of [max]
% 50.52/17.20 % (2442098)Cannot represent all propositional literals internally
% 50.52/17.20 % (2442098)Refutation not found, incomplete strategy
% 50.52/17.20 % (2442098)------------------------------
% 50.52/17.20 % (2442098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.52/17.20 % (2442098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.52/17.20 % (2442098)CaDiCaL version: 2.1.3
% 50.52/17.20 % (2442098)Termination reason: Refutation not found, incomplete strategy
% 50.52/17.20 % (2442098)Time elapsed: 0.892 s
% 50.52/17.20 % (2442098)Peak memory usage: 58 MB
% 50.52/17.20 % (2442098)Instructions burned: 1851 (million)
% 50.52/17.20 % (2442098)------------------------------
% 50.52/17.20 % (2442098)------------------------------
% 50.52/17.20 % (2442102)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=312821248:i=14134_2881 on theBenchmark for (2881ds/14134Mi)
% 50.52/17.20 % (2442102) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2442011-2442102"...
% 50.52/17.20 % (2442102)...printing done.
% 50.52/17.20 % (2442102)Refutation found. Thanks to Tanya!
% 50.52/17.20 % SZS status Theorem for theBenchmark
% 50.52/17.20 % SZS output start Proof for theBenchmark
% See solution above
% 118.14/17.22 % (2442102)------------------------------
% 118.14/17.22 % (2442102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.14/17.22 % (2442102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.14/17.22 % (2442102)CaDiCaL version: 2.1.3
% 118.14/17.22 % (2442102)Termination reason: Refutation
% 118.14/17.22 % (2442102)Time elapsed: 4.925 s
% 118.14/17.22 % (2442102)Peak memory usage: 88 MB
% 118.14/17.22 % (2442102)Instructions burned: 8887 (million)
% 118.14/17.22 % (2442011)Success in time 16.976 s
% 118.14/17.22 % Vampire exiting
%------------------------------------------------------------------------------