%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR101+3 : 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 : n011.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 244.05s 37.18s
% Output : Refutation 244.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 5
% Syntax : Number of formulae : 31 ( 13 unt; 0 def)
% Number of atoms : 69 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 64 ( 26 ~; 28 |; 5 &)
% ( 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 : 38 ( 37 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_26635) ).
fof(f26457,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+2.ax',kb_SUMO_26636) ).
fof(f145109,axiom,
s__subclass(s__Class32_2,s__Class32_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_8) ).
fof(f145110,axiom,
s__subclass(s__Class32_3,s__Class32_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_9) ).
fof(f145111,conjecture,
! [X0] :
( s__instance(X0,s__Class32_2)
=> s__instance(X0,s__Class32_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145112,negated_conjecture,
~ ! [X0] :
( s__instance(X0,s__Class32_2)
=> s__instance(X0,s__Class32_1) ),
inference(negated_conjecture,[status(cth)],[f145111]) ).
fof(f154471,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f154472,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,[],[f26457]) ).
fof(f154473,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,[],[f154472]) ).
fof(f168512,plain,
? [X0] :
( ~ s__instance(X0,s__Class32_1)
& s__instance(X0,s__Class32_2) ),
inference(ennf_transformation,[],[f145112]) ).
fof(f191282,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f154471]) ).
fof(f191283,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f154471]) ).
fof(f191284,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f154473]) ).
fof(f315082,plain,
s__subclass(s__Class32_2,s__Class32_3),
inference(cnf_transformation,[],[f145109]) ).
fof(f315083,plain,
s__subclass(s__Class32_3,s__Class32_1),
inference(cnf_transformation,[],[f145110]) ).
fof(f315084,plain,
s__instance(sK3001,s__Class32_2),
inference(cnf_transformation,[],[f168512]) ).
fof(f315085,plain,
~ s__instance(sK3001,s__Class32_1),
inference(cnf_transformation,[],[f168512]) ).
fof(f331255,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191283]) ).
fof(f331256,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191282]) ).
fof(f331257,plain,
! [X2,X0,X1] :
( s__instance(X0,s__SetOrClass)
| s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(consistent_polarity_flipping,[],[f191284]) ).
fof(f440809,plain,
~ s__subclass(s__Class32_2,s__Class32_3),
inference(consistent_polarity_flipping,[],[f315082]) ).
fof(f440810,plain,
~ s__subclass(s__Class32_3,s__Class32_1),
inference(consistent_polarity_flipping,[],[f315083]) ).
fof(f440811,plain,
s__instance(sK3001,s__Class32_1),
inference(consistent_polarity_flipping,[],[f315085]) ).
fof(f440812,plain,
~ s__instance(sK3001,s__Class32_2),
inference(consistent_polarity_flipping,[],[f315084]) ).
fof(f1349936,plain,
! [X2,X0,X1] :
( s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f331257,f331255]) ).
fof(f1349937,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f1349936,f331256]) ).
fof(f1352719,plain,
! [X0] :
( s__subclass(X0,s__Class32_1)
| s__instance(sK3001,X0) ),
inference(resolution,[],[f1349937,f440811]) ).
fof(f1352729,plain,
s__instance(sK3001,s__Class32_3),
inference(resolution,[],[f1352719,f440810]) ).
fof(f1352731,plain,
! [X0] :
( s__subclass(X0,s__Class32_3)
| s__instance(sK3001,X0) ),
inference(resolution,[],[f1352729,f1349937]) ).
fof(f1352735,plain,
s__instance(sK3001,s__Class32_2),
inference(resolution,[],[f1352731,f440809]) ).
fof(f1352736,plain,
$false,
inference(forward_subsumption_resolution,[],[f1352735,f440812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR101+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n011.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 22:50:46 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.23 Running first-order model finding
% 0.08/0.23 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
% 25.34/6.22 % (3866111)Will run a generic schedule for satisfiability detection.
% 25.34/6.22 % (3866117)% WARNING: option uhcvi not known.
% 25.34/6.22 % (3866116)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3395601592_2972 on theBenchmark for (2972ds/0Mi)
% 25.34/6.22 % (3866119)dis+10_1_sil=32000:sp=arity:random_seed=2190910836:i=103:fgj=on_2972 on theBenchmark for (2972ds/103Mi)
% 25.34/6.22 % (3866117)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=379754169:i=135531:add=off:rawr=on_2972 on theBenchmark for (2972ds/135531Mi)
% 25.34/6.22 % (3866118)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4183955150:i=88024:add=on:rawr=on_2972 on theBenchmark for (2972ds/88024Mi)
% 25.34/6.22 % (3866120)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2903463944:i=116_2972 on theBenchmark for (2972ds/116Mi)
% 25.34/6.22 % (3866121)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3864876379:i=131_2972 on theBenchmark for (2972ds/131Mi)
% 25.34/6.22 % (3866124)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4034227334:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2972 on theBenchmark for (2972ds/159Mi)
% 25.34/6.22 % (3866119)Instruction limit reached!
% 25.34/6.22 % (3866119)------------------------------
% 25.34/6.22 % (3866119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.34/6.22 % (3866119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.34/6.22 % (3866119)CaDiCaL version: 2.1.3
% 25.34/6.22 % (3866119)Termination reason: Instruction limit
% 25.34/6.22 % (3866119)Termination phase: Preprocessing 1
% 25.34/6.22 % (3866119)Time elapsed: 0.041 s
% 25.34/6.22 % (3866119)Peak memory usage: 155 MB
% 25.34/6.22 % (3866119)Instructions burned: 104 (million)
% 25.34/6.22 % (3866130)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3004468167:i=714:nm=2_2971 on theBenchmark for (2971ds/714Mi)
% 25.34/6.22 % (3866120)Instruction limit reached!
% 25.34/6.22 % (3866120)------------------------------
% 25.34/6.22 % (3866120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.34/6.22 % (3866120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.34/6.22 % (3866120)CaDiCaL version: 2.1.3
% 25.34/6.22 % (3866120)Termination reason: Instruction limit
% 25.34/6.22 % (3866120)Termination phase: Preprocessing 1
% 25.34/6.22 % (3866120)Time elapsed: 0.086 s
% 25.34/6.22 % (3866120)Peak memory usage: 155 MB
% 25.34/6.22 % (3866120)Instructions burned: 116 (million)
% 25.34/6.22 % (3866121)Instruction limit reached!
% 25.34/6.22 % (3866121)------------------------------
% 25.34/6.22 % (3866121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.34/6.22 % (3866121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.34/6.22 % (3866121)CaDiCaL version: 2.1.3
% 25.34/6.22 % (3866121)Termination reason: Instruction limit
% 25.34/6.22 % (3866121)Termination phase: Preprocessing 1
% 25.34/6.22 % (3866121)Time elapsed: 0.086 s
% 25.34/6.22 % (3866121)Peak memory usage: 155 MB
% 25.34/6.22 % (3866121)Instructions burned: 131 (million)
% 25.34/6.22 % (3866124)Instruction limit reached!
% 25.34/6.22 % (3866124)------------------------------
% 25.34/6.22 % (3866124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.34/6.22 % (3866124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.34/6.22 % (3866124)CaDiCaL version: 2.1.3
% 25.34/6.22 % (3866124)Termination reason: Instruction limit
% 25.34/6.22 % (3866124)Termination phase: Preprocessing 1
% 25.34/6.22 % (3866124)Time elapsed: 0.105 s
% 25.34/6.22 % (3866124)Peak memory usage: 155 MB
% 25.34/6.22 % (3866124)Instructions burned: 159 (million)
% 25.34/6.22 % (3866132)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2365026703:i=131:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/131Mi)
% 25.34/6.22 % (3866133)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=3438137231:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2970 on theBenchmark for (2970ds/684Mi)
% 25.34/6.22 % (3866136)ott-21_1_sil=16000:fs=off:random_seed=3829519312:i=180:av=off:fsr=off_2970 on theBenchmark for (2970ds/180Mi)
% 25.34/6.22 % (3866132)Instruction limit reached!
% 25.34/6.22 % (3866132)------------------------------
% 25.34/6.22 % (3866132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.34/6.22 % (3866132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866132)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866132)Termination reason: Instruction limit
% 51.59/10.03 % (3866132)Termination phase: Preprocessing 1
% 51.59/10.03 % (3866132)Time elapsed: 0.083 s
% 51.59/10.03 % (3866132)Peak memory usage: 155 MB
% 51.59/10.03 % (3866132)Instructions burned: 131 (million)
% 51.59/10.03 % (3866138)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3049400354:i=477:bd=all_2969 on theBenchmark for (2969ds/477Mi)
% 51.59/10.03 % (3866136)Instruction limit reached!
% 51.59/10.03 % (3866136)------------------------------
% 51.59/10.03 % (3866136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866136)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866136)Termination reason: Instruction limit
% 51.59/10.03 % (3866136)Termination phase: Preprocessing 1
% 51.59/10.03 % (3866136)Time elapsed: 0.124 s
% 51.59/10.03 % (3866136)Peak memory usage: 155 MB
% 51.59/10.03 % (3866136)Instructions burned: 181 (million)
% 51.59/10.03 % (3866130)Instruction limit reached!
% 51.59/10.03 % (3866130)------------------------------
% 51.59/10.03 % (3866130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866130)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866130)Termination reason: Instruction limit
% 51.59/10.03 % (3866130)Termination phase: Unused predicate definition removal
% 51.59/10.03 % (3866130)Time elapsed: 0.243 s
% 51.59/10.03 % (3866130)Peak memory usage: 189 MB
% 51.59/10.03 % (3866130)Instructions burned: 718 (million)
% 51.59/10.03 % (3866140)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1605017053:fmbsr=1.3:i=865:ins=25_2968 on theBenchmark for (2968ds/865Mi)
% 51.59/10.03 % (3866142)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3732352837:i=1179_2968 on theBenchmark for (2968ds/1179Mi)
% 51.59/10.03 % (3866133)Instruction limit reached!
% 51.59/10.03 % (3866133)------------------------------
% 51.59/10.03 % (3866133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866133)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866133)Termination reason: Instruction limit
% 51.59/10.03 % (3866133)Termination phase: Preprocessing 1
% 51.59/10.03 % (3866133)Time elapsed: 0.383 s
% 51.59/10.03 % (3866133)Peak memory usage: 158 MB
% 51.59/10.03 % (3866133)Instructions burned: 684 (million)
% 51.59/10.03 % (3866144)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2206714842:i=889:ins=1_2966 on theBenchmark for (2966ds/889Mi)
% 51.59/10.03 % (3866138)Instruction limit reached!
% 51.59/10.03 % (3866138)------------------------------
% 51.59/10.03 % (3866138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866138)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866138)Termination reason: Instruction limit
% 51.59/10.03 % (3866138)Termination phase: Naming
% 51.59/10.03 % (3866138)Time elapsed: 0.338 s
% 51.59/10.03 % (3866138)Peak memory usage: 164 MB
% 51.59/10.03 % (3866138)Instructions burned: 478 (million)
% 51.59/10.03 % (3866146)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=398879098:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2965 on theBenchmark for (2965ds/692Mi)
% 51.59/10.03 % (3866142)Instruction limit reached!
% 51.59/10.03 % (3866142)------------------------------
% 51.59/10.03 % (3866142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.59/10.03 % (3866142)CaDiCaL version: 2.1.3
% 51.59/10.03 % (3866142)Termination reason: Instruction limit
% 51.59/10.03 % (3866142)Termination phase: Property scanning
% 51.59/10.03 % (3866142)Time elapsed: 0.421 s
% 51.59/10.03 % (3866142)Peak memory usage: 185 MB
% 51.59/10.03 % (3866142)Instructions burned: 1182 (million)
% 51.59/10.03 % (3866148)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2909413309:i=879:kws=inv_precedence:fsr=off_2964 on theBenchmark for (2964ds/879Mi)
% 51.59/10.03 % (3866140)Instruction limit reached!
% 51.59/10.03 % (3866140)------------------------------
% 51.59/10.03 % (3866140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.59/10.03 % (3866140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866140)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866140)Termination reason: Instruction limit
% 82.10/14.30 % (3866140)Termination phase: Preprocessing 2
% 82.10/14.30 % (3866140)Time elapsed: 0.523 s
% 82.10/14.30 % (3866140)Peak memory usage: 203 MB
% 82.10/14.30 % (3866140)Instructions burned: 868 (million)
% 82.10/14.30 % (3866150)fmb+10_1_sil=64000:random_seed=1215223120:i=22061:nm=2:gsp=on_2963 on theBenchmark for (2963ds/22061Mi)
% 82.10/14.30 % (3866146)Instruction limit reached!
% 82.10/14.30 % (3866146)------------------------------
% 82.10/14.30 % (3866146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866146)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866146)Termination reason: Instruction limit
% 82.10/14.30 % (3866146)Termination phase: Preprocessing 1
% 82.10/14.30 % (3866146)Time elapsed: 0.403 s
% 82.10/14.30 % (3866146)Peak memory usage: 158 MB
% 82.10/14.30 % (3866146)Instructions burned: 693 (million)
% 82.10/14.30 % (3866152)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=998070213:i=9515:nm=5_2961 on theBenchmark for (2961ds/9515Mi)
% 82.10/14.30 % (3866148)Instruction limit reached!
% 82.10/14.30 % (3866148)------------------------------
% 82.10/14.30 % (3866148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866148)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866148)Termination reason: Instruction limit
% 82.10/14.30 % (3866148)Termination phase: NewCNF
% 82.10/14.30 % (3866148)Time elapsed: 0.309 s
% 82.10/14.30 % (3866148)Peak memory usage: 178 MB
% 82.10/14.30 % (3866148)Instructions burned: 885 (million)
% 82.10/14.30 % (3866144)Instruction limit reached!
% 82.10/14.30 % (3866144)------------------------------
% 82.10/14.30 % (3866144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866144)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866144)Termination reason: Instruction limit
% 82.10/14.30 % (3866144)Termination phase: Preprocessing 2
% 82.10/14.30 % (3866144)Time elapsed: 0.545 s
% 82.10/14.30 % (3866144)Peak memory usage: 194 MB
% 82.10/14.30 % (3866144)Instructions burned: 889 (million)
% 82.10/14.30 % (3866154)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1445133026:fmbsr=1.7:i=920_2960 on theBenchmark for (2960ds/920Mi)
% 82.10/14.30 % (3866156)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1253966320:i=5131_2960 on theBenchmark for (2960ds/5131Mi)
% 82.10/14.30 % (3866154)Instruction limit reached!
% 82.10/14.30 % (3866154)------------------------------
% 82.10/14.30 % (3866154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866154)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866154)Termination reason: Instruction limit
% 82.10/14.30 % (3866154)Termination phase: Preprocessing 2
% 82.10/14.30 % (3866154)Time elapsed: 0.337 s
% 82.10/14.30 % (3866154)Peak memory usage: 197 MB
% 82.10/14.30 % (3866154)Instructions burned: 923 (million)
% 82.10/14.30 % (3866158)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1368450051:i=1472:ins=7:fdi=8:gsp=on_2957 on theBenchmark for (2957ds/1472Mi)
% 82.10/14.30 % (3866158)Instruction limit reached!
% 82.10/14.30 % (3866158)------------------------------
% 82.10/14.30 % (3866158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866158)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866158)Termination reason: Instruction limit
% 82.10/14.30 % (3866158)Termination phase: Property scanning
% 82.10/14.30 % (3866158)Time elapsed: 0.489 s
% 82.10/14.30 % (3866158)Peak memory usage: 185 MB
% 82.10/14.30 % (3866158)Instructions burned: 1473 (million)
% 82.10/14.30 % (3866160)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2844295753:i=6324_2952 on theBenchmark for (2952ds/6324Mi)
% 82.10/14.30 % (3866156)Instruction limit reached!
% 82.10/14.30 % (3866156)------------------------------
% 82.10/14.30 % (3866156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.10/14.30 % (3866156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.10/14.30 % (3866156)CaDiCaL version: 2.1.3
% 82.10/14.30 % (3866156)Termination reason: Instruction limit
% 134.64/21.63 % (3866156)Termination phase: Saturation
% 134.64/21.63 % (3866156)Time elapsed: 2.020 s
% 134.64/21.63 % (3866156)Peak memory usage: 200 MB
% 134.64/21.63 % (3866156)Instructions burned: 5131 (million)
% 134.64/21.63 % (3866162)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4067216608:fmbsr=2.30978:i=2174_2939 on theBenchmark for (2939ds/2174Mi)
% 134.64/21.63 % (3866160)Instruction limit reached!
% 134.64/21.63 % (3866160)------------------------------
% 134.64/21.63 % (3866160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866160)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866160)Termination reason: Instruction limit
% 134.64/21.63 % (3866160)Termination phase: Property scanning
% 134.64/21.63 % (3866160)Time elapsed: 1.921 s
% 134.64/21.63 % (3866160)Peak memory usage: 298 MB
% 134.64/21.63 % (3866160)Instructions burned: 6326 (million)
% 134.64/21.63 % (3866164)ott-2_1_sil=16000:newcnf=on:random_seed=2664080633:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2932 on theBenchmark for (2932ds/869Mi)
% 134.64/21.63 % (3866164)Instruction limit reached!
% 134.64/21.63 % (3866164)------------------------------
% 134.64/21.63 % (3866164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866164)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866164)Termination reason: Instruction limit
% 134.64/21.63 % (3866164)Termination phase: NewCNF
% 134.64/21.63 % (3866164)Time elapsed: 0.301 s
% 134.64/21.63 % (3866164)Peak memory usage: 178 MB
% 134.64/21.63 % (3866164)Instructions burned: 871 (million)
% 134.64/21.63 % (3866166)ott+10_1_sil=32000:tgt=ground:random_seed=3165748622:i=5114:av=off_2929 on theBenchmark for (2929ds/5114Mi)
% 134.64/21.63 % (3866162)Instruction limit reached!
% 134.64/21.63 % (3866162)------------------------------
% 134.64/21.63 % (3866162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866162)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866162)Termination reason: Instruction limit
% 134.64/21.63 % (3866162)Termination phase: Property scanning
% 134.64/21.63 % (3866162)Time elapsed: 1.156 s
% 134.64/21.63 % (3866162)Peak memory usage: 241 MB
% 134.64/21.63 % (3866162)Instructions burned: 2175 (million)
% 134.64/21.63 % (3866168)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=213139647:i=54282_2927 on theBenchmark for (2927ds/54282Mi)
% 134.64/21.63 % (3866152)Instruction limit reached!
% 134.64/21.63 % (3866152)------------------------------
% 134.64/21.63 % (3866152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866152)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866152)Termination reason: Instruction limit
% 134.64/21.63 % (3866152)Termination phase: Finite model building preprocessing
% 134.64/21.63 % (3866152)Time elapsed: 4.605 s
% 134.64/21.63 % (3866152)Peak memory usage: 341 MB
% 134.64/21.63 % (3866152)Instructions burned: 9518 (million)
% 134.64/21.63 % (3866170)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4220680682:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 134.64/21.63 % (3866166)Instruction limit reached!
% 134.64/21.63 % (3866166)------------------------------
% 134.64/21.63 % (3866166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866166)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866166)Termination reason: Instruction limit
% 134.64/21.63 % (3866166)Termination phase: Saturation
% 134.64/21.63 % (3866166)Time elapsed: 1.555 s
% 134.64/21.63 % (3866166)Peak memory usage: 248 MB
% 134.64/21.63 % (3866166)Instructions burned: 5116 (million)
% 134.64/21.63 % (3866172)dis+21_1_sil=32000:sas=cadical:random_seed=4158182367:i=3773:amm=off_2913 on theBenchmark for (2913ds/3773Mi)
% 134.64/21.63 % (3866172)Instruction limit reached!
% 134.64/21.63 % (3866172)------------------------------
% 134.64/21.63 % (3866172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.64/21.63 % (3866172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.64/21.63 % (3866172)CaDiCaL version: 2.1.3
% 134.64/21.63 % (3866172)Termination reason: Instruction limit
% 134.64/21.63 % (3866172)Termination phase: Saturation
% 134.64/21.63 % (3866172)Time elapsed: 1.112 s
% 134.64/21.63 % (3866172)Peak memory usage: 210 MB
% 134.64/21.63 % (3866172)Instructions burned: 3775 (million)
% 168.00/26.37 % (3866174)ott+11_1_sil=16000:gs=on:random_seed=972689862:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2901 on theBenchmark for (2901ds/2251Mi)
% 168.00/26.37 % Detected minimum model sizes of [617]
% 168.00/26.37 % Detected maximum model sizes of [max]
% 168.00/26.37 % (3866150)Cannot represent all propositional literals internally
% 168.00/26.37 % (3866150)Refutation not found, incomplete strategy
% 168.00/26.37 % (3866150)------------------------------
% 168.00/26.37 % (3866150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.00/26.37 % (3866150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.00/26.37 % (3866150)CaDiCaL version: 2.1.3
% 168.00/26.37 % (3866150)Termination reason: Refutation not found, incomplete strategy
% 168.00/26.37 % (3866150)Time elapsed: 6.577 s
% 168.00/26.37 % (3866150)Peak memory usage: 388 MB
% 168.00/26.37 % (3866150)Instructions burned: 13611 (million)
% 168.00/26.37 % (3866170)Instruction limit reached!
% 168.00/26.37 % (3866170)------------------------------
% 168.00/26.37 % (3866170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.00/26.37 % (3866170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.00/26.37 % (3866170)CaDiCaL version: 2.1.3
% 168.00/26.37 % (3866170)Termination reason: Instruction limit
% 168.00/26.37 % (3866170)Termination phase: Saturation
% 168.00/26.37 % (3866170)Time elapsed: 1.821 s
% 168.00/26.37 % (3866170)Peak memory usage: 205 MB
% 168.00/26.37 % (3866170)Instructions burned: 3514 (million)
% 168.00/26.37 % (3866176)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2193279747:fmbsr=1.6:i=67534_2896 on theBenchmark for (2896ds/67534Mi)
% 168.00/26.37 % (3866150)------------------------------
% 168.00/26.37 % (3866150)------------------------------
% 168.00/26.37 % (3866174)Instruction limit reached!
% 168.00/26.37 % (3866174)------------------------------
% 168.00/26.37 % (3866174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.00/26.37 % (3866174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.00/26.37 % (3866174)CaDiCaL version: 2.1.3
% 168.00/26.37 % (3866174)Termination reason: Instruction limit
% 168.00/26.37 % (3866174)Termination phase: Property scanning
% 168.00/26.37 % (3866174)Time elapsed: 0.738 s
% 168.00/26.37 % (3866174)Peak memory usage: 188 MB
% 168.00/26.37 % (3866174)Instructions burned: 2251 (million)
% 168.00/26.37 % (3866179)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2607296661:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 168.00/26.37 % (3866178)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2129144077:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2894 on theBenchmark for (2894ds/4591Mi)
% 168.00/26.37 % Detected minimum model sizes of [617]
% 168.00/26.37 % Detected maximum model sizes of [max]
% 168.00/26.37 % (3866116)Cannot represent all propositional literals internally
% 168.00/26.37 % (3866116)Refutation not found, incomplete strategy
% 168.00/26.37 % (3866116)------------------------------
% 168.00/26.37 % (3866116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.00/26.37 % (3866116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.00/26.37 % (3866116)CaDiCaL version: 2.1.3
% 168.00/26.37 % (3866116)Termination reason: Refutation not found, incomplete strategy
% 168.00/26.37 % (3866116)Time elapsed: 8.375 s
% 168.00/26.37 % (3866116)Peak memory usage: 466 MB
% 168.00/26.37 % (3866116)Instructions burned: 17207 (million)
% 168.00/26.37 % (3866116)------------------------------
% 168.00/26.37 % (3866116)------------------------------
% 168.00/26.37 % (3866182)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4255940908:i=5211_2884 on theBenchmark for (2884ds/5211Mi)
% 168.00/26.37 % (3866178)Instruction limit reached!
% 168.00/26.37 % (3866178)------------------------------
% 168.00/26.37 % (3866178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.00/26.37 % (3866178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.00/26.37 % (3866178)CaDiCaL version: 2.1.3
% 168.00/26.37 % (3866178)Termination reason: Instruction limit
% 168.00/26.37 % (3866178)Termination phase: Saturation
% 168.00/26.37 % (3866178)Time elapsed: 2.465 s
% 168.00/26.37 % (3866178)Peak memory usage: 238 MB
% 168.00/26.37 % (3866178)Instructions burned: 4592 (million)
% 168.00/26.37 % (3866184)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2708831934:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi)
% 168.00/26.37 % (3866182)Instruction limit reached!
% 168.00/26.37 % (3866182)------------------------------
% 168.00/26.37 % (3866182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.60/35.49 % (3866182)CaDiCaL version: 2.1.3
% 232.60/35.49 % (3866182)Termination reason: Instruction limit
% 232.60/35.49 % (3866182)Termination phase: Saturation
% 232.60/35.49 % (3866182)Time elapsed: 2.526 s
% 232.60/35.49 % (3866182)Peak memory usage: 239 MB
% 232.60/35.49 % (3866182)Instructions burned: 5212 (million)
% 232.60/35.49 % (3866186)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3146323149:fmbsr=2:i=46332_2859 on theBenchmark for (2859ds/46332Mi)
% 232.60/35.49 % Detected minimum model sizes of [617]
% 232.60/35.49 % Detected maximum model sizes of [max]
% 232.60/35.49 % (3866168)Cannot represent all propositional literals internally
% 232.60/35.49 % (3866168)Refutation not found, incomplete strategy
% 232.60/35.49 % (3866168)------------------------------
% 232.60/35.49 % (3866168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.60/35.49 % (3866168)CaDiCaL version: 2.1.3
% 232.60/35.49 % (3866168)Termination reason: Refutation not found, incomplete strategy
% 232.60/35.49 % (3866168)Time elapsed: 8.388 s
% 232.60/35.49 % (3866168)Peak memory usage: 463 MB
% 232.60/35.49 % (3866168)Instructions burned: 17147 (million)
% 232.60/35.49 % (3866168)------------------------------
% 232.60/35.49 % (3866168)------------------------------
% 232.60/35.49 % (3866190)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3401200660:i=14071_2840 on theBenchmark for (2840ds/14071Mi)
% 232.60/35.49 % (3866184)Instruction limit reached!
% 232.60/35.49 % (3866184)------------------------------
% 232.60/35.49 % (3866184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.60/35.49 % (3866184)CaDiCaL version: 2.1.3
% 232.60/35.49 % (3866184)Termination reason: Instruction limit
% 232.60/35.49 % (3866184)Termination phase: Property scanning
% 232.60/35.49 % (3866184)Time elapsed: 3.141 s
% 232.60/35.49 % (3866184)Peak memory usage: 301 MB
% 232.60/35.49 % (3866184)Instructions burned: 5497 (million)
% 232.60/35.49 % (3866192)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3237231738:i=22565:add=on:rawr=on_2837 on theBenchmark for (2837ds/22565Mi)
% 232.60/35.49 % Detected minimum model sizes of [617]
% 232.60/35.49 % Detected maximum model sizes of [max]
% 232.60/35.49 % (3866176)Cannot represent all propositional literals internally
% 232.60/35.49 % (3866176)Refutation not found, incomplete strategy
% 232.60/35.49 % (3866176)------------------------------
% 232.60/35.49 % (3866176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.60/35.49 % (3866176)CaDiCaL version: 2.1.3
% 232.60/35.49 % (3866176)Termination reason: Refutation not found, incomplete strategy
% 232.60/35.49 % (3866176)Time elapsed: 7.313 s
% 232.60/35.49 % (3866176)Peak memory usage: 415 MB
% 232.60/35.49 % (3866176)Instructions burned: 15709 (million)
% 232.60/35.49 % (3866176)------------------------------
% 232.60/35.49 % (3866176)------------------------------
% 232.60/35.49 % (3866194)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=970068268:i=8173:av=off_2819 on theBenchmark for (2819ds/8173Mi)
% 232.60/35.49 % (3866194)Instruction limit reached!
% 232.60/35.49 % (3866194)------------------------------
% 232.60/35.49 % (3866194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.60/35.49 % (3866194)CaDiCaL version: 2.1.3
% 232.60/35.49 % (3866194)Termination reason: Instruction limit
% 232.60/35.49 % (3866194)Termination phase: Saturation
% 232.60/35.49 % (3866194)Time elapsed: 2.690 s
% 232.60/35.49 % (3866194)Peak memory usage: 196 MB
% 232.60/35.49 % (3866194)Instructions burned: 8173 (million)
% 232.60/35.49 % (3866196)dis+10_16:1_sil=16000:random_seed=583516833:i=9155:fsr=off_2792 on theBenchmark for (2792ds/9155Mi)
% 232.60/35.49 % Detected minimum model sizes of [617]
% 232.60/35.49 % Detected maximum model sizes of [max]
% 232.60/35.49 % (3866186)Cannot represent all propositional literals internally
% 232.60/35.49 % (3866186)Refutation not found, incomplete strategy
% 232.60/35.49 % (3866186)------------------------------
% 232.60/35.49 % (3866186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.60/35.49 % (3866186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866186)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866186)Termination reason: Refutation not found, incomplete strategy
% 231.73/37.06 % (3866186)Time elapsed: 7.284 s
% 231.73/37.06 % (3866186)Peak memory usage: 415 MB
% 231.73/37.06 % (3866186)Instructions burned: 15709 (million)
% 231.73/37.06 % (3866186)------------------------------
% 231.73/37.06 % (3866186)------------------------------
% 231.73/37.06 % (3866198)ott-3_8_sil=64000:random_seed=3942470426:i=20139:bs=on_2783 on theBenchmark for (2783ds/20139Mi)
% 231.73/37.06 % (3866179)Instruction limit reached!
% 231.73/37.06 % (3866179)------------------------------
% 231.73/37.06 % (3866179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866179)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866179)Termination reason: Instruction limit
% 231.73/37.06 % (3866179)Termination phase: Saturation
% 231.73/37.06 % (3866179)Time elapsed: 11.581 s
% 231.73/37.06 % (3866179)Peak memory usage: 352 MB
% 231.73/37.06 % (3866179)Instructions burned: 29340 (million)
% 231.73/37.06 % (3866200)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4003027356:fmbsr=2:i=32576_2777 on theBenchmark for (2777ds/32576Mi)
% 231.73/37.06 % (3866192)Instruction limit reached!
% 231.73/37.06 % (3866192)------------------------------
% 231.73/37.06 % (3866192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866192)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866192)Termination reason: Instruction limit
% 231.73/37.06 % (3866192)Termination phase: Saturation
% 231.73/37.06 % (3866192)Time elapsed: 6.277 s
% 231.73/37.06 % (3866192)Peak memory usage: 196 MB
% 231.73/37.06 % (3866192)Instructions burned: 22565 (million)
% 231.73/37.06 % (3866190)Instruction limit reached!
% 231.73/37.06 % (3866190)------------------------------
% 231.73/37.06 % (3866190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866190)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866190)Termination reason: Instruction limit
% 231.73/37.06 % (3866190)Termination phase: Finite model building preprocessing
% 231.73/37.06 % (3866190)Time elapsed: 6.641 s
% 231.73/37.06 % (3866190)Peak memory usage: 391 MB
% 231.73/37.06 % (3866190)Instructions burned: 14073 (million)
% 231.73/37.06 % (3866202)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3890899865:i=11404_2773 on theBenchmark for (2773ds/11404Mi)
% 231.73/37.06 % (3866204)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2191666950:i=14134_2773 on theBenchmark for (2773ds/14134Mi)
% 231.73/37.06 % (3866118)Instruction limit reached!
% 231.73/37.06 % (3866118)------------------------------
% 231.73/37.06 % (3866118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866118)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866118)Termination reason: Instruction limit
% 231.73/37.06 % (3866118)Termination phase: Saturation
% 231.73/37.06 % (3866118)Time elapsed: 22.015 s
% 231.73/37.06 % (3866118)Peak memory usage: 205 MB
% 231.73/37.06 % (3866118)Instructions burned: 88026 (million)
% 231.73/37.06 % (3866206)dis+33_16_sil=32000:sac=on:random_seed=847557513:i=15851:nm=0_2751 on theBenchmark for (2751ds/15851Mi)
% 231.73/37.06 % (3866196)Instruction limit reached!
% 231.73/37.06 % (3866196)------------------------------
% 231.73/37.06 % (3866196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866196)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866196)Termination reason: Instruction limit
% 231.73/37.06 % (3866196)Termination phase: Saturation
% 231.73/37.06 % (3866196)Time elapsed: 5.357 s
% 231.73/37.06 % (3866196)Peak memory usage: 270 MB
% 231.73/37.06 % (3866196)Instructions burned: 9157 (million)
% 231.73/37.06 % (3866202)Instruction limit reached!
% 231.73/37.06 % (3866202)------------------------------
% 231.73/37.06 % (3866202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 231.73/37.06 % (3866202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.73/37.06 % (3866202)CaDiCaL version: 2.1.3
% 231.73/37.06 % (3866202)Termination reason: Instruction limit
% 231.73/37.06 % (3866202)Termination phase: Saturation
% 231.73/37.06 % (3866202)Time elapsed: 3.491 s
% 231.73/37.06 % (3866202)Peak memory usage: 199 MB
% 231.73/37.06 % (3866202)Instructions burned: 11405 (million)
% 244.05/37.17 % (3866208)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2525171631:avsq=on:i=17627:add=on:amm=off_2738 on theBenchmark for (2738ds/17627Mi)
% 244.05/37.17 % (3866209)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=523520721:s2a=on:i=53295_2738 on theBenchmark for (2738ds/53295Mi)
% 244.05/37.17 % Detected minimum model sizes of [617]
% 244.05/37.17 % Detected maximum model sizes of [max]
% 244.05/37.17 % (3866200)Cannot represent all propositional literals internally
% 244.05/37.17 % (3866200)Refutation not found, incomplete strategy
% 244.05/37.17 % (3866200)------------------------------
% 244.05/37.17 % (3866200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.17 % (3866200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.17 % (3866200)CaDiCaL version: 2.1.3
% 244.05/37.17 % (3866200)Termination reason: Refutation not found, incomplete strategy
% 244.05/37.17 % (3866200)Time elapsed: 4.694 s
% 244.05/37.17 % (3866200)Peak memory usage: 452 MB
% 244.05/37.17 % (3866200)Instructions burned: 16984 (million)
% 244.05/37.17 % (3866200)------------------------------
% 244.05/37.17 % (3866200)------------------------------
% 244.05/37.17 % (3866212)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1489019947:i=26857:ins=20_2728 on theBenchmark for (2728ds/26857Mi)
% 244.05/37.17 % Detected minimum model sizes of [617]
% 244.05/37.17 % Detected maximum model sizes of [max]
% 244.05/37.17 % (3866212)Cannot represent all propositional literals internally
% 244.05/37.17 % (3866212)Refutation not found, incomplete strategy
% 244.05/37.17 % (3866212)------------------------------
% 244.05/37.17 % (3866212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.17 % (3866212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.17 % (3866212)CaDiCaL version: 2.1.3
% 244.05/37.17 % (3866212)Termination reason: Refutation not found, incomplete strategy
% 244.05/37.17 % (3866212)Time elapsed: 3.842 s
% 244.05/37.17 % (3866212)Peak memory usage: 406 MB
% 244.05/37.17 % (3866212)Instructions burned: 14584 (million)
% 244.05/37.17 % (3866208)Instruction limit reached!
% 244.05/37.17 % (3866208)------------------------------
% 244.05/37.17 % (3866208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.17 % (3866208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.17 % (3866208)CaDiCaL version: 2.1.3
% 244.05/37.17 % (3866208)Termination reason: Instruction limit
% 244.05/37.17 % (3866208)Termination phase: Saturation
% 244.05/37.17 % (3866208)Time elapsed: 4.922 s
% 244.05/37.17 % (3866208)Peak memory usage: 197 MB
% 244.05/37.17 % (3866208)Instructions burned: 17629 (million)
% 244.05/37.17 % (3866214)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1039449613:i=28120:bs=on:fsr=off_2688 on theBenchmark for (2688ds/28120Mi)
% 244.05/37.17 % (3866212)------------------------------
% 244.05/37.17 % (3866212)------------------------------
% 244.05/37.17 % (3866216)fmb+10_1_sil=256000:fmbss=7:random_seed=2310602577:fmbsr=1.6:i=182295_2687 on theBenchmark for (2687ds/182295Mi)
% 244.05/37.17 % (3866204)Instruction limit reached!
% 244.05/37.17 % (3866204)------------------------------
% 244.05/37.17 % (3866204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.17 % (3866204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.17 % (3866204)CaDiCaL version: 2.1.3
% 244.05/37.18 % (3866204)Termination reason: Instruction limit
% 244.05/37.18 % (3866204)Termination phase: Saturation
% 244.05/37.18 % (3866204)Time elapsed: 10.336 s
% 244.05/37.18 % (3866204)Peak memory usage: 284 MB
% 244.05/37.18 % (3866204)Instructions burned: 14134 (million)
% 244.05/37.18 % (3866218)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3624253653:i=44625:gsp=on_2669 on theBenchmark for (2669ds/44625Mi)
% 244.05/37.18 % Detected minimum model sizes of [617]
% 244.05/37.18 % Detected maximum model sizes of [max]
% 244.05/37.18 % (3866216)Cannot represent all propositional literals internally
% 244.05/37.18 % (3866216)Refutation not found, incomplete strategy
% 244.05/37.18 % (3866216)------------------------------
% 244.05/37.18 % (3866216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.18 % (3866216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.18 % (3866216)CaDiCaL version: 2.1.3
% 244.05/37.18 % (3866216)Termination reason: Refutation not found, incomplete strategy
% 244.05/37.18 % (3866216)Time elapsed: 3.855 s
% 244.05/37.18 % (3866216)Peak memory usage: 406 MB
% 244.05/37.18 % (3866216)Instructions burned: 14564 (million)
% 244.05/37.18 % (3866216)------------------------------
% 244.05/37.18 % (3866216)------------------------------
% 244.05/37.18 % (3866220)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=39326298:i=160505_2647 on theBenchmark for (2647ds/160505Mi)
% 244.05/37.18 % (3866206)Instruction limit reached!
% 244.05/37.18 % (3866206)------------------------------
% 244.05/37.18 % (3866206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.18 % (3866206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.18 % (3866206)CaDiCaL version: 2.1.3
% 244.05/37.18 % (3866206)Termination reason: Instruction limit
% 244.05/37.18 % (3866206)Termination phase: Saturation
% 244.05/37.18 % (3866206)Time elapsed: 10.583 s
% 244.05/37.18 % (3866206)Peak memory usage: 306 MB
% 244.05/37.18 % (3866206)Instructions burned: 15851 (million)
% 244.05/37.18 % (3866222)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2511881191:fmbsr=1.3:i=225729_2644 on theBenchmark for (2644ds/225729Mi)
% 244.05/37.18 % (3866117) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3866111-3866117"...
% 244.05/37.18 % (3866117)...printing done.
% 244.05/37.18 % (3866117)Refutation found. Thanks to Tanya!
% 244.05/37.18 % SZS status Theorem for theBenchmark
% 244.05/37.18 % SZS output start Proof for theBenchmark
% See solution above
% 244.05/37.18 % (3866117)------------------------------
% 244.05/37.18 % (3866117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.05/37.18 % (3866117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.05/37.18 % (3866117)CaDiCaL version: 2.1.3
% 244.05/37.18 % (3866117)Termination reason: Refutation
% 244.05/37.18 % (3866117)Time elapsed: 33.583 s
% 244.05/37.18 % (3866117)Peak memory usage: 536 MB
% 244.05/37.18 % (3866117)Instructions burned: 61490 (million)
% 244.05/37.18 % (3866111)Success in time 36.825 s
% 244.05/37.18 % Vampire exiting
%------------------------------------------------------------------------------