%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR101+2 : 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 : n004.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:15 AM UTC 2026
% Result : Theorem 0.18s 21.90s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 27 ( 9 unt; 0 def)
% Number of atoms : 65 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 77 ( 39 ~; 27 |; 6 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 29 ( 28 !; 1 ?)
% 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(f37989,axiom,
s__subclass(s__Class32_2,s__Class32_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_8) ).
fof(f37990,axiom,
s__subclass(s__Class32_3,s__Class32_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_9) ).
fof(f37991,conjecture,
! [X0] :
( s__instance(X0,s__Class32_2)
=> s__instance(X0,s__Class32_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f37992,negated_conjecture,
~ ! [X0] :
( s__instance(X0,s__Class32_2)
=> s__instance(X0,s__Class32_1) ),
inference(negated_conjecture,[status(cth)],[f37991]) ).
fof(f38259,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f38260,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(f38261,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,[],[f38260]) ).
fof(f48360,plain,
? [X0] :
( ~ s__instance(X0,s__Class32_1)
& s__instance(X0,s__Class32_2) ),
inference(ennf_transformation,[],[f37992]) ).
fof(f49891,plain,
( ~ s__instance(sK1514,s__Class32_1)
& s__instance(sK1514,s__Class32_2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1514]),skolemize(X0,sK1514)],[f48360]) ).
fof(f49921,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f38259]) ).
fof(f49922,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f38259]) ).
fof(f49923,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,[],[f38261]) ).
fof(f91058,plain,
s__subclass(s__Class32_2,s__Class32_3),
inference(cnf_transformation,[],[f37989]) ).
fof(f91059,plain,
s__subclass(s__Class32_3,s__Class32_1),
inference(cnf_transformation,[],[f37990]) ).
fof(f91060,plain,
s__instance(sK1514,s__Class32_2),
inference(cnf_transformation,[],[f49891]) ).
fof(f91061,plain,
~ s__instance(sK1514,s__Class32_1),
inference(cnf_transformation,[],[f49891]) ).
fof(f380102,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_1)
| ~ s__instance(sK1514,X0)
| ~ s__instance(s__Class32_1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f49923,f91061]) ).
fof(f380113,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_1)
| ~ s__instance(sK1514,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f380102,f49921]) ).
fof(f380842,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_1)
| ~ s__instance(sK1514,X0) ),
inference(forward_subsumption_resolution,[],[f380113,f49922]) ).
fof(f381572,plain,
~ s__instance(sK1514,s__Class32_3),
inference(resolution,[],[f380842,f91059]) ).
fof(f381573,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_3)
| ~ s__instance(sK1514,X0)
| ~ s__instance(s__Class32_3,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[],[f381572,f49923]) ).
fof(f381574,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_3)
| ~ s__instance(sK1514,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f381573,f49921]) ).
fof(f381575,plain,
! [X0] :
( ~ s__subclass(X0,s__Class32_3)
| ~ s__instance(sK1514,X0) ),
inference(forward_subsumption_resolution,[],[f381574,f49922]) ).
fof(f381578,plain,
~ s__instance(sK1514,s__Class32_2),
inference(resolution,[],[f381575,f91058]) ).
fof(f381579,plain,
$false,
inference(forward_subsumption_resolution,[],[f381578,f91060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR101+2 : 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.17 % Computer : n004.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 22:50:37 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 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
% 23.26/4.05 % (871789)Will run a generic schedule for satisfiability detection.
% 23.26/4.05 % (871798)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=196074453:i=116_2993 on theBenchmark for (2993ds/116Mi)
% 23.26/4.05 % (871795)% WARNING: option uhcvi not known.
% 23.26/4.05 % (871794)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=225798047_2993 on theBenchmark for (2993ds/0Mi)
% 23.26/4.05 % (871795)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=580969409:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi)
% 23.26/4.05 % (871796)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=556399950:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi)
% 23.26/4.05 % (871797)dis+10_1_sil=32000:sp=arity:random_seed=777931581:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi)
% 23.26/4.05 % (871799)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=944801523:i=131_2993 on theBenchmark for (2993ds/131Mi)
% 23.26/4.05 % (871800)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3768037572:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi)
% 23.26/4.05 % (871798)Instruction limit reached!
% 23.26/4.05 % (871798)------------------------------
% 23.26/4.05 % (871798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.26/4.05 % (871798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.05 % (871798)CaDiCaL version: 2.1.3
% 23.26/4.05 % (871798)Termination reason: Instruction limit
% 23.26/4.05 % (871798)Termination phase: NewCNF
% 23.26/4.05 % (871798)Time elapsed: 0.067 s
% 23.26/4.05 % (871798)Peak memory usage: 53 MB
% 23.26/4.05 % (871798)Instructions burned: 118 (million)
% 23.26/4.05 % (871808)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2994040807:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi)
% 23.26/4.05 % (871797)Instruction limit reached!
% 23.26/4.05 % (871797)------------------------------
% 23.26/4.05 % (871797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.26/4.05 % (871797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.05 % (871797)CaDiCaL version: 2.1.3
% 23.26/4.05 % (871797)Termination reason: Instruction limit
% 23.26/4.05 % (871797)Termination phase: Preprocessing 2
% 23.26/4.05 % (871797)Time elapsed: 0.086 s
% 23.26/4.05 % (871797)Peak memory usage: 51 MB
% 23.26/4.05 % (871797)Instructions burned: 104 (million)
% 23.26/4.05 % (871799)Instruction limit reached!
% 23.26/4.05 % (871799)------------------------------
% 23.26/4.05 % (871799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.26/4.05 % (871799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.05 % (871799)CaDiCaL version: 2.1.3
% 23.26/4.05 % (871799)Termination reason: Instruction limit
% 23.26/4.05 % (871799)Termination phase: Naming
% 23.26/4.05 % (871799)Time elapsed: 0.095 s
% 23.26/4.05 % (871799)Peak memory usage: 51 MB
% 23.26/4.05 % (871799)Instructions burned: 134 (million)
% 23.26/4.05 % (871810)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3113918626:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi)
% 23.26/4.05 % (871800)Instruction limit reached!
% 23.26/4.05 % (871800)------------------------------
% 23.26/4.05 % (871800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.26/4.05 % (871800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.05 % (871800)CaDiCaL version: 2.1.3
% 23.26/4.05 % (871800)Termination reason: Instruction limit
% 23.26/4.05 % (871800)Termination phase: Preprocessing 3
% 23.26/4.05 % (871800)Time elapsed: 0.108 s
% 23.26/4.05 % (871800)Peak memory usage: 52 MB
% 23.26/4.05 % (871800)Instructions burned: 161 (million)
% 23.26/4.05 % (871811)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=224339116:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi)
% 23.26/4.05 % (871813)ott-21_1_sil=16000:fs=off:random_seed=2484861433:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi)
% 23.26/4.05 % (871810)Instruction limit reached!
% 23.26/4.05 % (871810)------------------------------
% 23.26/4.05 % (871810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.26/4.05 % (871810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.05 % (871810)CaDiCaL version: 2.1.3
% 23.26/4.05 % (871810)Termination reason: Instruction limit
% 31.08/5.20 % (871810)Termination phase: Naming
% 31.08/5.20 % (871810)Time elapsed: 0.093 s
% 31.08/5.20 % (871810)Peak memory usage: 51 MB
% 31.08/5.20 % (871810)Instructions burned: 134 (million)
% 31.08/5.20 % (871816)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3681250843:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi)
% 31.08/5.20 % (871813)Instruction limit reached!
% 31.08/5.20 % (871813)------------------------------
% 31.08/5.20 % (871813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871813)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871813)Termination reason: Instruction limit
% 31.08/5.20 % (871813)Termination phase: Preprocessing 3
% 31.08/5.20 % (871813)Time elapsed: 0.125 s
% 31.08/5.20 % (871813)Peak memory usage: 52 MB
% 31.08/5.20 % (871813)Instructions burned: 181 (million)
% 31.08/5.20 % (871818)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4286402123:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi)
% 31.08/5.20 % (871808)Instruction limit reached!
% 31.08/5.20 % (871808)------------------------------
% 31.08/5.20 % (871808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871808)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871808)Termination reason: Instruction limit
% 31.08/5.20 % (871808)Termination phase: Clausification
% 31.08/5.20 % (871808)Time elapsed: 0.231 s
% 31.08/5.20 % (871808)Peak memory usage: 85 MB
% 31.08/5.20 % (871808)Instructions burned: 716 (million)
% 31.08/5.20 % (871820)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1346034237:i=1179_2990 on theBenchmark for (2990ds/1179Mi)
% 31.08/5.20 % (871811)Instruction limit reached!
% 31.08/5.20 % (871811)------------------------------
% 31.08/5.20 % (871811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871811)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871811)Termination reason: Instruction limit
% 31.08/5.20 % (871811)Termination phase: NewCNF
% 31.08/5.20 % (871811)Time elapsed: 0.328 s
% 31.08/5.20 % (871811)Peak memory usage: 61 MB
% 31.08/5.20 % (871811)Instructions burned: 685 (million)
% 31.08/5.20 % (871822)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=97054059:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi)
% 31.08/5.20 % (871816)Instruction limit reached!
% 31.08/5.20 % (871816)------------------------------
% 31.08/5.20 % (871816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871816)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871816)Termination reason: Instruction limit
% 31.08/5.20 % (871816)Termination phase: Equality resolution with deletion
% 31.08/5.20 % (871816)Time elapsed: 0.273 s
% 31.08/5.20 % (871816)Peak memory usage: 58 MB
% 31.08/5.20 % (871816)Instructions burned: 478 (million)
% 31.08/5.20 % (871824)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=1395657540:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2988 on theBenchmark for (2988ds/692Mi)
% 31.08/5.20 % (871820)Instruction limit reached!
% 31.08/5.20 % (871820)------------------------------
% 31.08/5.20 % (871820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871820)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871820)Termination reason: Instruction limit
% 31.08/5.20 % (871820)Termination phase: Saturation
% 31.08/5.20 % (871820)Time elapsed: 0.341 s
% 31.08/5.20 % (871820)Peak memory usage: 72 MB
% 31.08/5.20 % (871820)Instructions burned: 1180 (million)
% 31.08/5.20 % (871826)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2011902837:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi)
% 31.08/5.20 % (871818)Instruction limit reached!
% 31.08/5.20 % (871818)------------------------------
% 31.08/5.20 % (871818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.08/5.20 % (871818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.20 % (871818)CaDiCaL version: 2.1.3
% 31.08/5.20 % (871818)Termination reason: Instruction limit
% 31.08/5.20 % (871818)Termination phase: Property scanning
% 48.30/7.67 % (871818)Time elapsed: 0.456 s
% 48.30/7.67 % (871818)Peak memory usage: 89 MB
% 48.30/7.67 % (871818)Instructions burned: 866 (million)
% 48.30/7.67 % (871828)fmb+10_1_sil=64000:random_seed=733869056:i=22061:nm=2:gsp=on_2985 on theBenchmark for (2985ds/22061Mi)
% 48.30/7.67 % (871824)Instruction limit reached!
% 48.30/7.67 % (871824)------------------------------
% 48.30/7.67 % (871824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871824)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871824)Termination reason: Instruction limit
% 48.30/7.67 % (871824)Termination phase: NewCNF
% 48.30/7.67 % (871824)Time elapsed: 0.322 s
% 48.30/7.67 % (871824)Peak memory usage: 61 MB
% 48.30/7.67 % (871824)Instructions burned: 693 (million)
% 48.30/7.67 % (871830)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2259281675:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 48.30/7.67 % (871826)Instruction limit reached!
% 48.30/7.67 % (871826)------------------------------
% 48.30/7.67 % (871826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871826)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871826)Termination reason: Instruction limit
% 48.30/7.67 % (871826)Termination phase: Property scanning
% 48.30/7.67 % (871826)Time elapsed: 0.222 s
% 48.30/7.67 % (871826)Peak memory usage: 62 MB
% 48.30/7.67 % (871826)Instructions burned: 883 (million)
% 48.30/7.67 % (871832)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=829025169:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 48.30/7.67 % (871822)Instruction limit reached!
% 48.30/7.67 % (871822)------------------------------
% 48.30/7.67 % (871822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871822)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871822)Termination reason: Instruction limit
% 48.30/7.67 % (871822)Termination phase: Property scanning
% 48.30/7.67 % (871822)Time elapsed: 0.470 s
% 48.30/7.67 % (871822)Peak memory usage: 89 MB
% 48.30/7.67 % (871822)Instructions burned: 890 (million)
% 48.30/7.67 % (871834)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1702158940:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 48.30/7.67 % (871832)Instruction limit reached!
% 48.30/7.67 % (871832)------------------------------
% 48.30/7.67 % (871832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871832)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871832)Termination reason: Instruction limit
% 48.30/7.67 % (871832)Termination phase: Property scanning
% 48.30/7.67 % (871832)Time elapsed: 0.267 s
% 48.30/7.67 % (871832)Peak memory usage: 89 MB
% 48.30/7.67 % (871832)Instructions burned: 924 (million)
% 48.30/7.67 % (871836)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3950581918:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 48.30/7.67 % (871836)Instruction limit reached!
% 48.30/7.67 % (871836)------------------------------
% 48.30/7.67 % (871836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871836)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871836)Termination reason: Instruction limit
% 48.30/7.67 % (871836)Termination phase: Saturation
% 48.30/7.67 % (871836)Time elapsed: 0.438 s
% 48.30/7.67 % (871836)Peak memory usage: 79 MB
% 48.30/7.67 % (871836)Instructions burned: 1474 (million)
% 48.30/7.67 % (871838)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4085481741:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 48.30/7.67 % Detected minimum model sizes of [447]
% 48.30/7.67 % Detected maximum model sizes of [max]
% 48.30/7.67 % (871794)Cannot represent all propositional literals internally
% 48.30/7.67 % (871794)Refutation not found, incomplete strategy
% 48.30/7.67 % (871794)------------------------------
% 48.30/7.67 % (871794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.30/7.67 % (871794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.30/7.67 % (871794)CaDiCaL version: 2.1.3
% 48.30/7.67 % (871794)Termination reason: Refutation not found, incomplete strategy
% 48.30/7.67 % (871794)Time elapsed: 3.169 s
% 48.30/7.67 % (871794)Peak memory usage: 172 MB
% 68.65/10.55 % (871794)Instructions burned: 6845 (million)
% 68.65/10.55 % (871794)------------------------------
% 68.65/10.55 % (871794)------------------------------
% 68.65/10.55 % (871840)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2347725137:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 68.65/10.55 % (871838)Instruction limit reached!
% 68.65/10.55 % (871838)------------------------------
% 68.65/10.55 % (871838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.65/10.55 % (871838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.55 % (871838)CaDiCaL version: 2.1.3
% 68.65/10.55 % (871838)Termination reason: Instruction limit
% 68.65/10.55 % (871838)Termination phase: Finite model building preprocessing
% 68.65/10.55 % (871838)Time elapsed: 1.603 s
% 68.65/10.55 % (871838)Peak memory usage: 167 MB
% 68.65/10.55 % (871838)Instructions burned: 6325 (million)
% 68.65/10.55 % (871842)ott-2_1_sil=16000:newcnf=on:random_seed=3955835544:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2960 on theBenchmark for (2960ds/869Mi)
% 68.65/10.55 % Detected minimum model sizes of [447]
% 68.65/10.55 % Detected maximum model sizes of [max]
% 68.65/10.55 % (871828)Cannot represent all propositional literals internally
% 68.65/10.55 % (871828)Refutation not found, incomplete strategy
% 68.65/10.55 % (871828)------------------------------
% 68.65/10.55 % (871828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.65/10.55 % (871828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.55 % (871828)CaDiCaL version: 2.1.3
% 68.65/10.55 % (871828)Termination reason: Refutation not found, incomplete strategy
% 68.65/10.55 % (871828)Time elapsed: 2.605 s
% 68.65/10.55 % (871828)Peak memory usage: 153 MB
% 68.65/10.55 % (871828)Instructions burned: 5781 (million)
% 68.65/10.55 % (871828)------------------------------
% 68.65/10.55 % (871828)------------------------------
% 68.65/10.55 % (871844)ott+10_1_sil=32000:tgt=ground:random_seed=3737637579:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 68.65/10.55 % (871842)Instruction limit reached!
% 68.65/10.55 % (871842)------------------------------
% 68.65/10.55 % (871842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.65/10.55 % (871842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.55 % (871842)CaDiCaL version: 2.1.3
% 68.65/10.55 % (871842)Termination reason: Instruction limit
% 68.65/10.55 % (871842)Termination phase: Property scanning
% 68.65/10.55 % (871842)Time elapsed: 0.218 s
% 68.65/10.55 % (871842)Peak memory usage: 62 MB
% 68.65/10.55 % (871842)Instructions burned: 870 (million)
% 68.65/10.55 % (871846)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=291455314:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 68.65/10.55 % Detected minimum model sizes of [447]
% 68.65/10.55 % Detected maximum model sizes of [max]
% 68.65/10.55 % (871830)Cannot represent all propositional literals internally
% 68.65/10.55 % (871830)Refutation not found, incomplete strategy
% 68.65/10.55 % (871830)------------------------------
% 68.65/10.55 % (871830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.65/10.55 % (871830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.55 % (871830)CaDiCaL version: 2.1.3
% 68.65/10.55 % (871830)Termination reason: Refutation not found, incomplete strategy
% 68.65/10.55 % (871830)Time elapsed: 2.770 s
% 68.65/10.55 % (871830)Peak memory usage: 157 MB
% 68.65/10.55 % (871830)Instructions burned: 5978 (million)
% 68.65/10.55 % (871830)------------------------------
% 68.65/10.55 % (871830)------------------------------
% 68.65/10.55 % (871834)Instruction limit reached!
% 68.65/10.55 % (871834)------------------------------
% 68.65/10.55 % (871834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.65/10.55 % (871834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.55 % (871834)CaDiCaL version: 2.1.3
% 68.65/10.55 % (871834)Termination reason: Instruction limit
% 68.65/10.55 % (871834)Termination phase: Saturation
% 68.65/10.55 % (871834)Time elapsed: 2.750 s
% 68.65/10.55 % (871834)Peak memory usage: 108 MB
% 68.65/10.55 % (871834)Instructions burned: 5133 (million)
% 68.65/10.55 % (871848)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3669444699:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi)
% 68.65/10.55 % (871849)dis+21_1_sil=32000:sas=cadical:random_seed=3132179063:i=3773:amm=off_2955 on theBenchmark for (2955ds/3773Mi)
% 68.65/10.55 % (871840)Instruction limit reached!
% 68.65/10.55 % (871840)------------------------------
% 68.65/10.55 % (871840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871840)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871840)Termination reason: Instruction limit
% 135.18/19.83 % (871840)Termination phase: Finite model building preprocessing
% 135.18/19.83 % (871840)Time elapsed: 1.052 s
% 135.18/19.83 % (871840)Peak memory usage: 116 MB
% 135.18/19.83 % (871840)Instructions burned: 2174 (million)
% 135.18/19.83 % (871852)ott+11_1_sil=16000:gs=on:random_seed=959334832:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2950 on theBenchmark for (2950ds/2251Mi)
% 135.18/19.83 % (871852)Instruction limit reached!
% 135.18/19.83 % (871852)------------------------------
% 135.18/19.83 % (871852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871852)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871852)Termination reason: Instruction limit
% 135.18/19.83 % (871852)Termination phase: Saturation
% 135.18/19.83 % (871852)Time elapsed: 0.842 s
% 135.18/19.83 % (871852)Peak memory usage: 65 MB
% 135.18/19.83 % (871852)Instructions burned: 2255 (million)
% 135.18/19.83 % (871854)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=885596977:fmbsr=1.6:i=67534_2941 on theBenchmark for (2941ds/67534Mi)
% 135.18/19.83 % Detected minimum model sizes of [447]
% 135.18/19.83 % Detected maximum model sizes of [max]
% 135.18/19.83 % (871846)Cannot represent all propositional literals internally
% 135.18/19.83 % (871846)Refutation not found, incomplete strategy
% 135.18/19.83 % (871846)------------------------------
% 135.18/19.83 % (871846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871846)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871846)Termination reason: Refutation not found, incomplete strategy
% 135.18/19.83 % (871846)Time elapsed: 1.777 s
% 135.18/19.83 % (871846)Peak memory usage: 172 MB
% 135.18/19.83 % (871846)Instructions burned: 6838 (million)
% 135.18/19.83 % (871846)------------------------------
% 135.18/19.83 % (871846)------------------------------
% 135.18/19.83 % (871856)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3482029586:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2939 on theBenchmark for (2939ds/4591Mi)
% 135.18/19.83 % (871848)Instruction limit reached!
% 135.18/19.83 % (871848)------------------------------
% 135.18/19.83 % (871848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871848)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871848)Termination reason: Instruction limit
% 135.18/19.83 % (871848)Termination phase: Saturation
% 135.18/19.83 % (871848)Time elapsed: 1.858 s
% 135.18/19.83 % (871848)Peak memory usage: 100 MB
% 135.18/19.83 % (871848)Instructions burned: 3512 (million)
% 135.18/19.83 % (871858)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=740950620:i=29340_2937 on theBenchmark for (2937ds/29340Mi)
% 135.18/19.83 % (871849)Instruction limit reached!
% 135.18/19.83 % (871849)------------------------------
% 135.18/19.83 % (871849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871849)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871849)Termination reason: Instruction limit
% 135.18/19.83 % (871849)Termination phase: Saturation
% 135.18/19.83 % (871849)Time elapsed: 1.910 s
% 135.18/19.83 % (871849)Peak memory usage: 101 MB
% 135.18/19.83 % (871849)Instructions burned: 3773 (million)
% 135.18/19.83 % (871860)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1735054440:i=5211_2936 on theBenchmark for (2936ds/5211Mi)
% 135.18/19.83 % (871844)Instruction limit reached!
% 135.18/19.83 % (871844)------------------------------
% 135.18/19.83 % (871844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 135.18/19.83 % (871844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.18/19.83 % (871844)CaDiCaL version: 2.1.3
% 135.18/19.83 % (871844)Termination reason: Instruction limit
% 135.18/19.83 % (871844)Termination phase: Saturation
% 135.18/19.83 % (871844)Time elapsed: 2.953 s
% 135.18/19.83 % (871844)Peak memory usage: 95 MB
% 135.18/19.83 % (871844)Instructions burned: 5116 (million)
% 135.18/19.83 % (871862)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3724517546:i=5497:nm=2_2928 on theBenchmark for (2928ds/5497Mi)
% 135.18/19.83 % (871856)Instruction limit reached!
% 85.93/21.85 % (871856)------------------------------
% 85.93/21.85 % (871856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871856)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871856)Termination reason: Instruction limit
% 85.93/21.85 % (871856)Termination phase: Saturation
% 85.93/21.85 % (871856)Time elapsed: 1.420 s
% 85.93/21.85 % (871856)Peak memory usage: 98 MB
% 85.93/21.85 % (871856)Instructions burned: 4594 (million)
% 85.93/21.85 % (871864)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2353646511:fmbsr=2:i=46332_2925 on theBenchmark for (2925ds/46332Mi)
% 85.93/21.85 % Detected minimum model sizes of [447]
% 85.93/21.85 % Detected maximum model sizes of [max]
% 85.93/21.85 % (871854)Cannot represent all propositional literals internally
% 85.93/21.85 % (871854)Refutation not found, incomplete strategy
% 85.93/21.85 % (871854)------------------------------
% 85.93/21.85 % (871854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871854)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871854)Termination reason: Refutation not found, incomplete strategy
% 85.93/21.85 % (871854)Time elapsed: 2.936 s
% 85.93/21.85 % (871854)Peak memory usage: 162 MB
% 85.93/21.85 % (871854)Instructions burned: 6557 (million)
% 85.93/21.85 % (871854)------------------------------
% 85.93/21.85 % (871854)------------------------------
% 85.93/21.85 % (871866)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1082438242:i=14071_2910 on theBenchmark for (2910ds/14071Mi)
% 85.93/21.85 % (871860)Instruction limit reached!
% 85.93/21.85 % (871860)------------------------------
% 85.93/21.85 % (871860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871860)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871860)Termination reason: Instruction limit
% 85.93/21.85 % (871860)Termination phase: Saturation
% 85.93/21.85 % (871860)Time elapsed: 2.604 s
% 85.93/21.85 % (871860)Peak memory usage: 112 MB
% 85.93/21.85 % (871860)Instructions burned: 5212 (million)
% 85.93/21.85 % (871868)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3977729793:i=22565:add=on:rawr=on_2910 on theBenchmark for (2910ds/22565Mi)
% 85.93/21.85 % Detected minimum model sizes of [447]
% 85.93/21.85 % Detected maximum model sizes of [max]
% 85.93/21.85 % (871864)Cannot represent all propositional literals internally
% 85.93/21.85 % (871864)Refutation not found, incomplete strategy
% 85.93/21.85 % (871864)------------------------------
% 85.93/21.85 % (871864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871864)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871864)Termination reason: Refutation not found, incomplete strategy
% 85.93/21.85 % (871864)Time elapsed: 1.602 s
% 85.93/21.85 % (871864)Peak memory usage: 162 MB
% 85.93/21.85 % (871864)Instructions burned: 6557 (million)
% 85.93/21.85 % (871864)------------------------------
% 85.93/21.85 % (871864)------------------------------
% 85.93/21.85 % (871870)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3878076363:i=8173:av=off_2908 on theBenchmark for (2908ds/8173Mi)
% 85.93/21.85 % (871862)Instruction limit reached!
% 85.93/21.85 % (871862)------------------------------
% 85.93/21.85 % (871862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871862)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871862)Termination reason: Instruction limit
% 85.93/21.85 % (871862)Termination phase: Finite model building preprocessing
% 85.93/21.85 % (871862)Time elapsed: 2.644 s
% 85.93/21.85 % (871862)Peak memory usage: 159 MB
% 85.93/21.85 % (871862)Instructions burned: 5498 (million)
% 85.93/21.85 % (871872)dis+10_16:1_sil=16000:random_seed=3380704326:i=9155:fsr=off_2902 on theBenchmark for (2902ds/9155Mi)
% 85.93/21.85 % (871870)Instruction limit reached!
% 85.93/21.85 % (871870)------------------------------
% 85.93/21.85 % (871870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.93/21.85 % (871870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.93/21.85 % (871870)CaDiCaL version: 2.1.3
% 85.93/21.85 % (871870)Termination reason: Instruction limit
% 85.93/21.85 % (871870)Termination phase: Saturation
% 0.18/21.90 % (871870)Time elapsed: 1.195 s
% 0.18/21.90 % (871870)Peak memory usage: 70 MB
% 0.18/21.90 % (871870)Instructions burned: 8174 (million)
% 0.18/21.90 % (871874)ott-3_8_sil=64000:random_seed=2360368862:i=20139:bs=on_2896 on theBenchmark for (2896ds/20139Mi)
% 0.18/21.90 % Detected minimum model sizes of [447]
% 0.18/21.90 % Detected maximum model sizes of [max]
% 0.18/21.90 % (871866)Cannot represent all propositional literals internally
% 0.18/21.90 % (871866)Refutation not found, incomplete strategy
% 0.18/21.90 % (871866)------------------------------
% 0.18/21.90 % (871866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871866)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871866)Termination reason: Refutation not found, incomplete strategy
% 0.18/21.90 % (871866)Time elapsed: 2.782 s
% 0.18/21.90 % (871866)Peak memory usage: 160 MB
% 0.18/21.90 % (871866)Instructions burned: 6104 (million)
% 0.18/21.90 % (871866)------------------------------
% 0.18/21.90 % (871866)------------------------------
% 0.18/21.90 % (871876)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3953536971:fmbsr=2:i=32576_2882 on theBenchmark for (2882ds/32576Mi)
% 0.18/21.90 % (871872)Instruction limit reached!
% 0.18/21.90 % (871872)------------------------------
% 0.18/21.90 % (871872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871872)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871872)Termination reason: Instruction limit
% 0.18/21.90 % (871872)Termination phase: Saturation
% 0.18/21.90 % (871872)Time elapsed: 4.385 s
% 0.18/21.90 % (871872)Peak memory usage: 115 MB
% 0.18/21.90 % (871872)Instructions burned: 9157 (million)
% 0.18/21.90 % (871878)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1887914552:i=11404_2857 on theBenchmark for (2857ds/11404Mi)
% 0.18/21.90 % Detected minimum model sizes of [447]
% 0.18/21.90 % Detected maximum model sizes of [max]
% 0.18/21.90 % (871876)Cannot represent all propositional literals internally
% 0.18/21.90 % (871876)Refutation not found, incomplete strategy
% 0.18/21.90 % (871876)------------------------------
% 0.18/21.90 % (871876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871876)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871876)Termination reason: Refutation not found, incomplete strategy
% 0.18/21.90 % (871876)Time elapsed: 3.181 s
% 0.18/21.90 % (871876)Peak memory usage: 171 MB
% 0.18/21.90 % (871876)Instructions burned: 6819 (million)
% 0.18/21.90 % (871876)------------------------------
% 0.18/21.90 % (871876)------------------------------
% 0.18/21.90 % (871880)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2233433384:i=14134_2849 on theBenchmark for (2849ds/14134Mi)
% 0.18/21.90 % (871874)Instruction limit reached!
% 0.18/21.90 % (871874)------------------------------
% 0.18/21.90 % (871874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871874)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871874)Termination reason: Instruction limit
% 0.18/21.90 % (871874)Termination phase: Saturation
% 0.18/21.90 % (871874)Time elapsed: 6.189 s
% 0.18/21.90 % (871874)Peak memory usage: 117 MB
% 0.18/21.90 % (871874)Instructions burned: 20140 (million)
% 0.18/21.90 % (871882)dis+33_16_sil=32000:sac=on:random_seed=1669997543:i=15851:nm=0_2834 on theBenchmark for (2834ds/15851Mi)
% 0.18/21.90 % (871878)Instruction limit reached!
% 0.18/21.90 % (871878)------------------------------
% 0.18/21.90 % (871878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871878)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871878)Termination reason: Instruction limit
% 0.18/21.90 % (871878)Termination phase: Saturation
% 0.18/21.90 % (871878)Time elapsed: 3.933 s
% 0.18/21.90 % (871878)Peak memory usage: 106 MB
% 0.18/21.90 % (871878)Instructions burned: 11406 (million)
% 0.18/21.90 % (871885)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3527482869:avsq=on:i=17627:add=on:amm=off_2818 on theBenchmark for (2818ds/17627Mi)
% 0.18/21.90 % (871868)Instruction limit reached!
% 0.18/21.90 % (871868)------------------------------
% 0.18/21.90 % (871868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871868)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871868)Termination reason: Instruction limit
% 0.18/21.90 % (871868)Termination phase: Saturation
% 0.18/21.90 % (871868)Time elapsed: 10.602 s
% 0.18/21.90 % (871868)Peak memory usage: 574 MB
% 0.18/21.90 % (871868)Instructions burned: 22565 (million)
% 0.18/21.90 % (871887)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=560358001:s2a=on:i=53295_2803 on theBenchmark for (2803ds/53295Mi)
% 0.18/21.90 % (871880) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-871789-871880"...
% 0.18/21.90 % (871882)Instruction limit reached!
% 0.18/21.90 % (871882)------------------------------
% 0.18/21.90 % (871882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871882)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871882)Termination reason: Instruction limit
% 0.18/21.90 % (871882)Termination phase: Saturation
% 0.18/21.90 % (871882)Time elapsed: 4.851 s
% 0.18/21.90 % (871882)Peak memory usage: 121 MB
% 0.18/21.90 % (871882)Instructions burned: 15852 (million)
% 0.18/21.90 % (871880)...printing done.
% 0.18/21.90 % (871880)Refutation found. Thanks to Tanya!
% 0.18/21.90 % SZS status Theorem for theBenchmark
% 0.18/21.90 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/21.90 % (871880)------------------------------
% 0.18/21.90 % (871880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.90 % (871880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.90 % (871880)CaDiCaL version: 2.1.3
% 0.18/21.90 % (871880)Termination reason: Refutation
% 0.18/21.90 % (871880)Time elapsed: 6.277 s
% 0.18/21.90 % (871880)Peak memory usage: 148 MB
% 0.18/21.90 % (871880)Instructions burned: 9832 (million)
% 0.18/21.90 % (871789)Success in time 21.643 s
% 0.18/21.90 % Vampire exiting
%------------------------------------------------------------------------------