%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR099+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:14 AM UTC 2026
% Result : Theorem 201.56s 31.16s
% Output : Refutation 201.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 22 ( 10 unt; 0 def)
% Number of atoms : 54 ( 13 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 58 ( 26 ~; 25 |; 4 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 22 ( 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_26635) ).
fof(f28085,axiom,
! [X0,X1] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__subclass(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_28267) ).
fof(f145103,axiom,
s__subclass(s__Class30_1,s__Reptile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f145104,axiom,
s__subclass(s__Reptile,s__Class30_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f145105,conjecture,
s__Class30_1 = s__Reptile,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145106,negated_conjecture,
s__Class30_1 != s__Reptile,
inference(negated_conjecture,[status(cth)],[f145105]) ).
fof(f145147,plain,
s__Reptile != s__Class30_1,
inference(flattening,[],[f145106]) ).
fof(f154466,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f156357,plain,
! [X0,X1] :
( X0 = X1
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f28085]) ).
fof(f156358,plain,
! [X0,X1] :
( X0 = X1
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f156357]) ).
fof(f191277,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f154466]) ).
fof(f193256,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X0)
| ~ s__subclass(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f156358]) ).
fof(f315070,plain,
s__subclass(s__Class30_1,s__Reptile),
inference(cnf_transformation,[],[f145103]) ).
fof(f315071,plain,
s__subclass(s__Reptile,s__Class30_1),
inference(cnf_transformation,[],[f145104]) ).
fof(f315072,plain,
s__Reptile != s__Class30_1,
inference(cnf_transformation,[],[f145147]) ).
fof(f332788,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191277]) ).
fof(f334612,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X0)
| ~ s__subclass(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f193256]) ).
fof(f1364644,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X0)
| ~ s__subclass(X0,X1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f334612,f332788]) ).
fof(f1364645,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X0)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f1364644,f332788]) ).
fof(f1406878,plain,
( ~ s__subclass(s__Reptile,s__Class30_1)
| s__Reptile = s__Class30_1 ),
inference(resolution,[],[f1364645,f315070]) ).
fof(f1406925,plain,
s__Reptile = s__Class30_1,
inference(forward_subsumption_resolution,[],[f1406878,f315071]) ).
fof(f1786939,plain,
$false,
inference(forward_subsumption_resolution,[],[f1406925,f315072]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR099+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.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:52:37 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.91/6.56 % (864089)Will run a generic schedule for satisfiability detection.
% 27.91/6.56 % (864096)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3550045806:i=88024:add=on:rawr=on_2972 on theBenchmark for (2972ds/88024Mi)
% 27.91/6.56 % (864095)% WARNING: option uhcvi not known.
% 27.91/6.56 % (864094)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3310397938_2972 on theBenchmark for (2972ds/0Mi)
% 27.91/6.56 % (864095)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=177070145:i=135531:add=off:rawr=on_2972 on theBenchmark for (2972ds/135531Mi)
% 27.91/6.56 % (864097)dis+10_1_sil=32000:sp=arity:random_seed=981969440:i=103:fgj=on_2972 on theBenchmark for (2972ds/103Mi)
% 27.91/6.56 % (864098)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=175082274:i=116_2972 on theBenchmark for (2972ds/116Mi)
% 27.91/6.56 % (864099)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2558391222:i=131_2972 on theBenchmark for (2972ds/131Mi)
% 27.91/6.56 % (864102)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=642524879:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2972 on theBenchmark for (2972ds/159Mi)
% 27.91/6.56 % (864097)Instruction limit reached!
% 27.91/6.56 % (864097)------------------------------
% 27.91/6.56 % (864097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.91/6.56 % (864097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/6.56 % (864097)CaDiCaL version: 2.1.3
% 27.91/6.56 % (864097)Termination reason: Instruction limit
% 27.91/6.56 % (864097)Termination phase: Preprocessing 1
% 27.91/6.56 % (864097)Time elapsed: 0.065 s
% 27.91/6.56 % (864097)Peak memory usage: 155 MB
% 27.91/6.56 % (864097)Instructions burned: 103 (million)
% 27.91/6.56 % (864098)Instruction limit reached!
% 27.91/6.56 % (864098)------------------------------
% 27.91/6.56 % (864098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.91/6.56 % (864098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/6.56 % (864098)CaDiCaL version: 2.1.3
% 27.91/6.56 % (864098)Termination reason: Instruction limit
% 27.91/6.56 % (864098)Termination phase: Preprocessing 1
% 27.91/6.56 % (864098)Time elapsed: 0.085 s
% 27.91/6.56 % (864098)Peak memory usage: 155 MB
% 27.91/6.56 % (864098)Instructions burned: 116 (million)
% 27.91/6.56 % (864099)Instruction limit reached!
% 27.91/6.56 % (864099)------------------------------
% 27.91/6.56 % (864099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.91/6.56 % (864099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/6.56 % (864099)CaDiCaL version: 2.1.3
% 27.91/6.56 % (864099)Termination reason: Instruction limit
% 27.91/6.56 % (864099)Termination phase: Preprocessing 1
% 27.91/6.56 % (864099)Time elapsed: 0.088 s
% 27.91/6.56 % (864099)Peak memory usage: 155 MB
% 27.91/6.56 % (864099)Instructions burned: 131 (million)
% 27.91/6.56 % (864108)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4226138753:i=714:nm=2_2971 on theBenchmark for (2971ds/714Mi)
% 27.91/6.56 % (864102)Instruction limit reached!
% 27.91/6.56 % (864102)------------------------------
% 27.91/6.56 % (864102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.91/6.56 % (864102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/6.56 % (864102)CaDiCaL version: 2.1.3
% 27.91/6.56 % (864102)Termination reason: Instruction limit
% 27.91/6.56 % (864102)Termination phase: Preprocessing 1
% 27.91/6.56 % (864102)Time elapsed: 0.106 s
% 27.91/6.56 % (864102)Peak memory usage: 155 MB
% 27.91/6.56 % (864102)Instructions burned: 160 (million)
% 27.91/6.56 % (864110)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=527602653:i=131:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/131Mi)
% 27.91/6.56 % (864111)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=2538044373:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2971 on theBenchmark for (2971ds/684Mi)
% 27.91/6.56 % (864114)ott-21_1_sil=16000:fs=off:random_seed=1789883548:i=180:av=off:fsr=off_2971 on theBenchmark for (2971ds/180Mi)
% 27.91/6.56 % (864110)Instruction limit reached!
% 27.91/6.56 % (864110)------------------------------
% 27.91/6.56 % (864110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.91/6.56 % (864110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/6.56 % (864110)CaDiCaL version: 2.1.3
% 27.91/6.56 % (864110)Termination reason: Instruction limit
% 58.93/10.98 % (864110)Termination phase: Preprocessing 1
% 58.93/10.98 % (864110)Time elapsed: 0.082 s
% 58.93/10.98 % (864110)Peak memory usage: 155 MB
% 58.93/10.98 % (864110)Instructions burned: 131 (million)
% 58.93/10.98 % (864116)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3961570089:i=477:bd=all_2970 on theBenchmark for (2970ds/477Mi)
% 58.93/10.98 % (864114)Instruction limit reached!
% 58.93/10.98 % (864114)------------------------------
% 58.93/10.98 % (864114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864114)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864114)Termination reason: Instruction limit
% 58.93/10.98 % (864114)Termination phase: Preprocessing 1
% 58.93/10.98 % (864114)Time elapsed: 0.120 s
% 58.93/10.98 % (864114)Peak memory usage: 155 MB
% 58.93/10.98 % (864114)Instructions burned: 180 (million)
% 58.93/10.98 % (864118)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=258182978:fmbsr=1.3:i=865:ins=25_2969 on theBenchmark for (2969ds/865Mi)
% 58.93/10.98 % (864111)Instruction limit reached!
% 58.93/10.98 % (864111)------------------------------
% 58.93/10.98 % (864111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864111)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864111)Termination reason: Instruction limit
% 58.93/10.98 % (864111)Termination phase: Preprocessing 1
% 58.93/10.98 % (864111)Time elapsed: 0.381 s
% 58.93/10.98 % (864111)Peak memory usage: 158 MB
% 58.93/10.98 % (864111)Instructions burned: 685 (million)
% 58.93/10.98 % (864108)Instruction limit reached!
% 58.93/10.98 % (864108)------------------------------
% 58.93/10.98 % (864108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864108)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864108)Termination reason: Instruction limit
% 58.93/10.98 % (864108)Termination phase: Unused predicate definition removal
% 58.93/10.98 % (864108)Time elapsed: 0.422 s
% 58.93/10.98 % (864108)Peak memory usage: 189 MB
% 58.93/10.98 % (864108)Instructions burned: 714 (million)
% 58.93/10.98 % (864120)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2778950973:i=1179_2967 on theBenchmark for (2967ds/1179Mi)
% 58.93/10.98 % (864121)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2285657071:i=889:ins=1_2967 on theBenchmark for (2967ds/889Mi)
% 58.93/10.98 % (864116)Instruction limit reached!
% 58.93/10.98 % (864116)------------------------------
% 58.93/10.98 % (864116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864116)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864116)Termination reason: Instruction limit
% 58.93/10.98 % (864116)Termination phase: Naming
% 58.93/10.98 % (864116)Time elapsed: 0.366 s
% 58.93/10.98 % (864116)Peak memory usage: 164 MB
% 58.93/10.98 % (864116)Instructions burned: 477 (million)
% 58.93/10.98 % (864124)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=2012794747:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2966 on theBenchmark for (2966ds/692Mi)
% 58.93/10.98 % (864118)Instruction limit reached!
% 58.93/10.98 % (864118)------------------------------
% 58.93/10.98 % (864118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864118)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864118)Termination reason: Instruction limit
% 58.93/10.98 % (864118)Termination phase: Preprocessing 2
% 58.93/10.98 % (864118)Time elapsed: 0.535 s
% 58.93/10.98 % (864118)Peak memory usage: 203 MB
% 58.93/10.98 % (864118)Instructions burned: 867 (million)
% 58.93/10.98 % (864126)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=566458158:i=879:kws=inv_precedence:fsr=off_2963 on theBenchmark for (2963ds/879Mi)
% 58.93/10.98 % (864124)Instruction limit reached!
% 58.93/10.98 % (864124)------------------------------
% 58.93/10.98 % (864124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.93/10.98 % (864124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.93/10.98 % (864124)CaDiCaL version: 2.1.3
% 58.93/10.98 % (864124)Termination reason: Instruction limit
% 84.83/14.63 % (864124)Termination phase: Preprocessing 1
% 84.83/14.63 % (864124)Time elapsed: 0.400 s
% 84.83/14.63 % (864124)Peak memory usage: 158 MB
% 84.83/14.63 % (864124)Instructions burned: 692 (million)
% 84.83/14.63 % (864128)fmb+10_1_sil=64000:random_seed=1425957520:i=22061:nm=2:gsp=on_2961 on theBenchmark for (2961ds/22061Mi)
% 84.83/14.63 % (864121)Instruction limit reached!
% 84.83/14.63 % (864121)------------------------------
% 84.83/14.63 % (864121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864121)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864121)Termination reason: Instruction limit
% 84.83/14.63 % (864121)Termination phase: Preprocessing 2
% 84.83/14.63 % (864121)Time elapsed: 0.572 s
% 84.83/14.63 % (864121)Peak memory usage: 194 MB
% 84.83/14.63 % (864121)Instructions burned: 890 (million)
% 84.83/14.63 % (864130)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=287378228:i=9515:nm=5_2960 on theBenchmark for (2960ds/9515Mi)
% 84.83/14.63 % (864120)Instruction limit reached!
% 84.83/14.63 % (864120)------------------------------
% 84.83/14.63 % (864120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864120)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864120)Termination reason: Instruction limit
% 84.83/14.63 % (864120)Termination phase: Property scanning
% 84.83/14.63 % (864120)Time elapsed: 0.730 s
% 84.83/14.63 % (864120)Peak memory usage: 185 MB
% 84.83/14.63 % (864120)Instructions burned: 1181 (million)
% 84.83/14.63 % (864132)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3360234498:fmbsr=1.7:i=920_2959 on theBenchmark for (2959ds/920Mi)
% 84.83/14.63 % (864126)Instruction limit reached!
% 84.83/14.63 % (864126)------------------------------
% 84.83/14.63 % (864126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864126)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864126)Termination reason: Instruction limit
% 84.83/14.63 % (864126)Termination phase: NewCNF
% 84.83/14.63 % (864126)Time elapsed: 0.515 s
% 84.83/14.63 % (864126)Peak memory usage: 178 MB
% 84.83/14.63 % (864126)Instructions burned: 880 (million)
% 84.83/14.63 % (864134)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2964980680:i=5131_2958 on theBenchmark for (2958ds/5131Mi)
% 84.83/14.63 % (864132)Instruction limit reached!
% 84.83/14.63 % (864132)------------------------------
% 84.83/14.63 % (864132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864132)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864132)Termination reason: Instruction limit
% 84.83/14.63 % (864132)Termination phase: Preprocessing 2
% 84.83/14.63 % (864132)Time elapsed: 0.562 s
% 84.83/14.63 % (864132)Peak memory usage: 197 MB
% 84.83/14.63 % (864132)Instructions burned: 922 (million)
% 84.83/14.63 % (864136)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1464636753:i=1472:ins=7:fdi=8:gsp=on_2953 on theBenchmark for (2953ds/1472Mi)
% 84.83/14.63 % (864136)Instruction limit reached!
% 84.83/14.63 % (864136)------------------------------
% 84.83/14.63 % (864136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864136)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864136)Termination reason: Instruction limit
% 84.83/14.63 % (864136)Termination phase: Property scanning
% 84.83/14.63 % (864136)Time elapsed: 0.807 s
% 84.83/14.63 % (864136)Peak memory usage: 185 MB
% 84.83/14.63 % (864136)Instructions burned: 1474 (million)
% 84.83/14.63 % (864138)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1304954945:i=6324_2945 on theBenchmark for (2945ds/6324Mi)
% 84.83/14.63 % (864134)Instruction limit reached!
% 84.83/14.63 % (864134)------------------------------
% 84.83/14.63 % (864134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 84.83/14.63 % (864134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.83/14.63 % (864134)CaDiCaL version: 2.1.3
% 84.83/14.63 % (864134)Termination reason: Instruction limit
% 84.83/14.63 % (864134)Termination phase: Saturation
% 84.83/14.63 % (864134)Time elapsed: 2.091 s
% 84.83/14.63 % (864134)Peak memory usage: 200 MB
% 84.83/14.63 % (864134)Instructions burned: 5133 (million)
% 84.83/14.63 % (864140)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2746136980:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 112.43/19.06 % (864140)Instruction limit reached!
% 112.43/19.06 % (864140)------------------------------
% 112.43/19.06 % (864140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864140)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864140)Termination reason: Instruction limit
% 112.43/19.06 % (864140)Termination phase: Property scanning
% 112.43/19.06 % (864140)Time elapsed: 1.139 s
% 112.43/19.06 % (864140)Peak memory usage: 241 MB
% 112.43/19.06 % (864140)Instructions burned: 2175 (million)
% 112.43/19.06 % (864142)ott-2_1_sil=16000:newcnf=on:random_seed=3325358354:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2925 on theBenchmark for (2925ds/869Mi)
% 112.43/19.06 % (864142)Instruction limit reached!
% 112.43/19.06 % (864142)------------------------------
% 112.43/19.06 % (864142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864142)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864142)Termination reason: Instruction limit
% 112.43/19.06 % (864142)Termination phase: NewCNF
% 112.43/19.06 % (864142)Time elapsed: 0.523 s
% 112.43/19.06 % (864142)Peak memory usage: 178 MB
% 112.43/19.06 % (864142)Instructions burned: 871 (million)
% 112.43/19.06 % (864144)ott+10_1_sil=32000:tgt=ground:random_seed=2964585690:i=5114:av=off_2919 on theBenchmark for (2919ds/5114Mi)
% 112.43/19.06 % (864130)Instruction limit reached!
% 112.43/19.06 % (864130)------------------------------
% 112.43/19.06 % (864130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864130)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864130)Termination reason: Instruction limit
% 112.43/19.06 % (864130)Termination phase: Finite model building preprocessing
% 112.43/19.06 % (864130)Time elapsed: 4.526 s
% 112.43/19.06 % (864130)Peak memory usage: 341 MB
% 112.43/19.06 % (864130)Instructions burned: 9517 (million)
% 112.43/19.06 % (864146)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3583080656:i=54282_2915 on theBenchmark for (2915ds/54282Mi)
% 112.43/19.06 % (864138)Instruction limit reached!
% 112.43/19.06 % (864138)------------------------------
% 112.43/19.06 % (864138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864138)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864138)Termination reason: Instruction limit
% 112.43/19.06 % (864138)Termination phase: Property scanning
% 112.43/19.06 % (864138)Time elapsed: 3.372 s
% 112.43/19.06 % (864138)Peak memory usage: 298 MB
% 112.43/19.06 % (864138)Instructions burned: 6326 (million)
% 112.43/19.06 % (864148)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2331896187:i=3512:aac=none_2910 on theBenchmark for (2910ds/3512Mi)
% 112.43/19.06 % Detected minimum model sizes of [617]
% 112.43/19.06 % Detected maximum model sizes of [max]
% 112.43/19.06 % (864128)Cannot represent all propositional literals internally
% 112.43/19.06 % (864128)Refutation not found, incomplete strategy
% 112.43/19.06 % (864128)------------------------------
% 112.43/19.06 % (864128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864128)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864128)Termination reason: Refutation not found, incomplete strategy
% 112.43/19.06 % (864128)Time elapsed: 6.336 s
% 112.43/19.06 % (864128)Peak memory usage: 388 MB
% 112.43/19.06 % (864128)Instructions burned: 13612 (million)
% 112.43/19.06 % (864128)------------------------------
% 112.43/19.06 % (864128)------------------------------
% 112.43/19.06 % (864150)dis+21_1_sil=32000:sas=cadical:random_seed=3558826254:i=3773:amm=off_2895 on theBenchmark for (2895ds/3773Mi)
% 112.43/19.06 % (864148)Instruction limit reached!
% 112.43/19.06 % (864148)------------------------------
% 112.43/19.06 % (864148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.43/19.06 % (864148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.43/19.06 % (864148)CaDiCaL version: 2.1.3
% 112.43/19.06 % (864148)Termination reason: Instruction limit
% 112.43/19.06 % (864148)Termination phase: Saturation
% 112.43/19.06 % (864148)Time elapsed: 1.761 s
% 112.43/19.06 % (864148)Peak memory usage: 204 MB
% 112.43/19.06 % (864148)Instructions burned: 3512 (million)
% 112.43/19.06 % (864152)ott+11_1_sil=16000:gs=on:random_seed=3904066539:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2892 on theBenchmark for (2892ds/2251Mi)
% 182.62/28.31 % (864144)Instruction limit reached!
% 182.62/28.31 % (864144)------------------------------
% 182.62/28.31 % (864144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864144)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864144)Termination reason: Instruction limit
% 182.62/28.31 % (864144)Termination phase: Saturation
% 182.62/28.31 % (864144)Time elapsed: 2.816 s
% 182.62/28.31 % (864144)Peak memory usage: 248 MB
% 182.62/28.31 % (864144)Instructions burned: 5114 (million)
% 182.62/28.31 % (864154)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2816732402:fmbsr=1.6:i=67534_2890 on theBenchmark for (2890ds/67534Mi)
% 182.62/28.31 % Detected minimum model sizes of [617]
% 182.62/28.31 % Detected maximum model sizes of [max]
% 182.62/28.31 % (864094)Cannot represent all propositional literals internally
% 182.62/28.31 % (864094)Refutation not found, incomplete strategy
% 182.62/28.31 % (864094)------------------------------
% 182.62/28.31 % (864094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864094)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864094)Termination reason: Refutation not found, incomplete strategy
% 182.62/28.31 % (864094)Time elapsed: 8.234 s
% 182.62/28.31 % (864094)Peak memory usage: 456 MB
% 182.62/28.31 % (864094)Instructions burned: 17046 (million)
% 182.62/28.31 % (864094)------------------------------
% 182.62/28.31 % (864094)------------------------------
% 182.62/28.31 % (864156)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1263616362:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2887 on theBenchmark for (2887ds/4591Mi)
% 182.62/28.31 % (864152)Instruction limit reached!
% 182.62/28.31 % (864152)------------------------------
% 182.62/28.31 % (864152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864152)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864152)Termination reason: Instruction limit
% 182.62/28.31 % (864152)Termination phase: Property scanning
% 182.62/28.31 % (864152)Time elapsed: 1.307 s
% 182.62/28.31 % (864152)Peak memory usage: 188 MB
% 182.62/28.31 % (864152)Instructions burned: 2252 (million)
% 182.62/28.31 % (864158)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=210420944:i=29340_2879 on theBenchmark for (2879ds/29340Mi)
% 182.62/28.31 % (864150)Instruction limit reached!
% 182.62/28.31 % (864150)------------------------------
% 182.62/28.31 % (864150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864150)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864150)Termination reason: Instruction limit
% 182.62/28.31 % (864150)Termination phase: Saturation
% 182.62/28.31 % (864150)Time elapsed: 2.002 s
% 182.62/28.31 % (864150)Peak memory usage: 209 MB
% 182.62/28.31 % (864150)Instructions burned: 3774 (million)
% 182.62/28.31 % (864160)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3403130199:i=5211_2874 on theBenchmark for (2874ds/5211Mi)
% 182.62/28.31 % (864156)Instruction limit reached!
% 182.62/28.31 % (864156)------------------------------
% 182.62/28.31 % (864156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864156)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864156)Termination reason: Instruction limit
% 182.62/28.31 % (864156)Termination phase: Saturation
% 182.62/28.31 % (864156)Time elapsed: 2.464 s
% 182.62/28.31 % (864156)Peak memory usage: 238 MB
% 182.62/28.31 % (864156)Instructions burned: 4592 (million)
% 182.62/28.31 % (864162)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2981382039:i=5497:nm=2_2861 on theBenchmark for (2861ds/5497Mi)
% 182.62/28.31 % (864096)Instruction limit reached!
% 182.62/28.31 % (864096)------------------------------
% 182.62/28.31 % (864096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 182.62/28.31 % (864096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.62/28.31 % (864096)CaDiCaL version: 2.1.3
% 182.62/28.31 % (864096)Termination reason: Instruction limit
% 182.62/28.31 % (864096)Termination phase: Saturation
% 182.62/28.31 % (864096)Time elapsed: 11.653 s
% 178.54/30.96 % (864096)Peak memory usage: 205 MB
% 178.54/30.96 % (864096)Instructions burned: 88032 (million)
% 178.54/30.96 % (864164)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1801484643:fmbsr=2:i=46332_2855 on theBenchmark for (2855ds/46332Mi)
% 178.54/30.96 % (864160)Instruction limit reached!
% 178.54/30.96 % (864160)------------------------------
% 178.54/30.96 % (864160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.54/30.96 % (864160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.54/30.96 % (864160)CaDiCaL version: 2.1.3
% 178.54/30.96 % (864160)Termination reason: Instruction limit
% 178.54/30.96 % (864160)Termination phase: Saturation
% 178.54/30.96 % (864160)Time elapsed: 2.474 s
% 178.54/30.96 % (864160)Peak memory usage: 239 MB
% 178.54/30.96 % (864160)Instructions burned: 5212 (million)
% 178.54/30.96 % (864166)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3498633937:i=14071_2849 on theBenchmark for (2849ds/14071Mi)
% 178.54/30.96 % Detected minimum model sizes of [617]
% 178.54/30.96 % Detected maximum model sizes of [max]
% 178.54/30.96 % (864146)Cannot represent all propositional literals internally
% 178.54/30.96 % (864146)Refutation not found, incomplete strategy
% 178.54/30.96 % (864146)------------------------------
% 178.54/30.96 % (864146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.54/30.96 % (864146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.54/30.96 % (864146)CaDiCaL version: 2.1.3
% 178.54/30.96 % (864146)Termination reason: Refutation not found, incomplete strategy
% 178.54/30.96 % (864146)Time elapsed: 8.201 s
% 178.54/30.96 % (864146)Peak memory usage: 457 MB
% 178.54/30.96 % (864146)Instructions burned: 17071 (million)
% 178.54/30.96 % (864146)------------------------------
% 178.54/30.96 % (864146)------------------------------
% 178.54/30.96 % (864162)Instruction limit reached!
% 178.54/30.96 % (864162)------------------------------
% 178.54/30.96 % (864162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.54/30.96 % (864162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.54/30.96 % (864162)CaDiCaL version: 2.1.3
% 178.54/30.96 % (864162)Termination reason: Instruction limit
% 178.54/30.96 % (864162)Termination phase: Property scanning
% 178.54/30.96 % (864162)Time elapsed: 3.157 s
% 178.54/30.96 % (864162)Peak memory usage: 301 MB
% 178.54/30.96 % (864162)Instructions burned: 5499 (million)
% 178.54/30.96 % (864168)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=494958148:i=22565:add=on:rawr=on_2829 on theBenchmark for (2829ds/22565Mi)
% 178.54/30.96 % (864169)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=951205198:i=8173:av=off_2829 on theBenchmark for (2829ds/8173Mi)
% 178.54/30.96 % Detected minimum model sizes of [617]
% 178.54/30.96 % Detected maximum model sizes of [max]
% 178.54/30.96 % (864154)Cannot represent all propositional literals internally
% 178.54/30.96 % (864154)Refutation not found, incomplete strategy
% 178.54/30.96 % (864154)------------------------------
% 178.54/30.96 % (864154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.54/30.96 % (864154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.54/30.96 % (864154)CaDiCaL version: 2.1.3
% 178.54/30.96 % (864154)Termination reason: Refutation not found, incomplete strategy
% 178.54/30.96 % (864154)Time elapsed: 7.257 s
% 178.54/30.96 % (864154)Peak memory usage: 415 MB
% 178.54/30.96 % (864154)Instructions burned: 15711 (million)
% 178.54/30.96 % (864154)------------------------------
% 178.54/30.96 % (864154)------------------------------
% 178.54/30.96 % (864172)dis+10_16:1_sil=16000:random_seed=684939981:i=9155:fsr=off_2815 on theBenchmark for (2815ds/9155Mi)
% 178.54/30.96 % Detected minimum model sizes of [617]
% 178.54/30.96 % Detected maximum model sizes of [max]
% 178.54/30.96 % (864164)Cannot represent all propositional literals internally
% 178.54/30.96 % (864164)Refutation not found, incomplete strategy
% 178.54/30.96 % (864164)------------------------------
% 178.54/30.96 % (864164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.54/30.96 % (864164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.54/30.96 % (864164)CaDiCaL version: 2.1.3
% 178.54/30.96 % (864164)Termination reason: Refutation not found, incomplete strategy
% 178.54/30.96 % (864164)Time elapsed: 4.169 s
% 178.54/30.96 % (864164)Peak memory usage: 415 MB
% 178.54/30.96 % (864164)Instructions burned: 15711 (million)
% 178.54/30.96 % (864164)------------------------------
% 178.54/30.96 % (864164)------------------------------
% 178.54/30.96 % (864174)ott-3_8_sil=64000:random_seed=139860092:i=20139:bs=on_2811 on theBenchmark for (2811ds/20139Mi)
% 201.56/31.16 % (864169)Instruction limit reached!
% 201.56/31.16 % (864169)------------------------------
% 201.56/31.16 % (864169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864169)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864169)Termination reason: Instruction limit
% 201.56/31.16 % (864169)Termination phase: Saturation
% 201.56/31.16 % (864169)Time elapsed: 2.726 s
% 201.56/31.16 % (864169)Peak memory usage: 196 MB
% 201.56/31.16 % (864169)Instructions burned: 8179 (million)
% 201.56/31.16 % (864176)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2479617502:fmbsr=2:i=32576_2801 on theBenchmark for (2801ds/32576Mi)
% 201.56/31.16 % (864166)Instruction limit reached!
% 201.56/31.16 % (864166)------------------------------
% 201.56/31.16 % (864166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864166)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864166)Termination reason: Instruction limit
% 201.56/31.16 % (864166)Termination phase: Finite model building preprocessing
% 201.56/31.16 % (864166)Time elapsed: 6.588 s
% 201.56/31.16 % (864166)Peak memory usage: 391 MB
% 201.56/31.16 % (864166)Instructions burned: 14073 (million)
% 201.56/31.16 % (864178)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2740680230:i=11404_2783 on theBenchmark for (2783ds/11404Mi)
% 201.56/31.16 % (864168)Instruction limit reached!
% 201.56/31.16 % (864168)------------------------------
% 201.56/31.16 % (864168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864168)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864168)Termination reason: Instruction limit
% 201.56/31.16 % (864168)Termination phase: Saturation
% 201.56/31.16 % (864168)Time elapsed: 6.375 s
% 201.56/31.16 % (864168)Peak memory usage: 196 MB
% 201.56/31.16 % (864168)Instructions burned: 22567 (million)
% 201.56/31.16 % (864180)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3802378865:i=14134_2765 on theBenchmark for (2765ds/14134Mi)
% 201.56/31.16 % (864172)Instruction limit reached!
% 201.56/31.16 % (864172)------------------------------
% 201.56/31.16 % (864172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864172)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864172)Termination reason: Instruction limit
% 201.56/31.16 % (864172)Termination phase: Saturation
% 201.56/31.16 % (864172)Time elapsed: 4.979 s
% 201.56/31.16 % (864172)Peak memory usage: 296 MB
% 201.56/31.16 % (864172)Instructions burned: 9157 (million)
% 201.56/31.16 % (864182)dis+33_16_sil=32000:sac=on:random_seed=413671809:i=15851:nm=0_2764 on theBenchmark for (2764ds/15851Mi)
% 201.56/31.16 % (864178)Instruction limit reached!
% 201.56/31.16 % (864178)------------------------------
% 201.56/31.16 % (864178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864178)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864178)Termination reason: Instruction limit
% 201.56/31.16 % (864178)Termination phase: Saturation
% 201.56/31.16 % (864178)Time elapsed: 3.452 s
% 201.56/31.16 % (864178)Peak memory usage: 199 MB
% 201.56/31.16 % (864178)Instructions burned: 11407 (million)
% 201.56/31.16 % (864184)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3192142088:avsq=on:i=17627:add=on:amm=off_2748 on theBenchmark for (2748ds/17627Mi)
% 201.56/31.16 % (864174)Instruction limit reached!
% 201.56/31.16 % (864174)------------------------------
% 201.56/31.16 % (864174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864174)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864174)Termination reason: Instruction limit
% 201.56/31.16 % (864174)Termination phase: Saturation
% 201.56/31.16 % (864174)Time elapsed: 8.479 s
% 201.56/31.16 % (864174)Peak memory usage: 291 MB
% 201.56/31.16 % (864174)Instructions burned: 20141 (million)
% 201.56/31.16 % (864186)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4131311210:s2a=on:i=53295_2726 on theBenchmark for (2726ds/53295Mi)
% 201.56/31.16 % Detected minimum model sizes of [617]
% 201.56/31.16 % Detected maximum model sizes of [max]
% 201.56/31.16 % (864176)Cannot represent all propositional literals internally
% 201.56/31.16 % (864176)Refutation not found, incomplete strategy
% 201.56/31.16 % (864176)------------------------------
% 201.56/31.16 % (864176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864176)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864176)Termination reason: Refutation not found, incomplete strategy
% 201.56/31.16 % (864176)Time elapsed: 8.247 s
% 201.56/31.16 % (864176)Peak memory usage: 452 MB
% 201.56/31.16 % (864176)Instructions burned: 16990 (million)
% 201.56/31.16 % (864176)------------------------------
% 201.56/31.16 % (864176)------------------------------
% 201.56/31.16 % (864188)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1348771910:i=26857:ins=20_2715 on theBenchmark for (2715ds/26857Mi)
% 201.56/31.16 % (864158)Instruction limit reached!
% 201.56/31.16 % (864158)------------------------------
% 201.56/31.16 % (864158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864158)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864158)Termination reason: Instruction limit
% 201.56/31.16 % (864158)Termination phase: Saturation
% 201.56/31.16 % (864158)Time elapsed: 16.487 s
% 201.56/31.16 % (864158)Peak memory usage: 942 MB
% 201.56/31.16 % (864158)Instructions burned: 29343 (million)
% 201.56/31.16 % (864190)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1880589909:i=28120:bs=on:fsr=off_2712 on theBenchmark for (2712ds/28120Mi)
% 201.56/31.16 % (864184)Instruction limit reached!
% 201.56/31.16 % (864184)------------------------------
% 201.56/31.16 % (864184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864184)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864184)Termination reason: Instruction limit
% 201.56/31.16 % (864184)Termination phase: Saturation
% 201.56/31.16 % (864184)Time elapsed: 5.0000 s
% 201.56/31.16 % (864184)Peak memory usage: 197 MB
% 201.56/31.16 % (864184)Instructions burned: 17627 (million)
% 201.56/31.16 % (864192)fmb+10_1_sil=256000:fmbss=7:random_seed=963677267:fmbsr=1.6:i=182295_2697 on theBenchmark for (2697ds/182295Mi)
% 201.56/31.16 % (864095) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-864089-864095"...
% 201.56/31.16 % (864095)...printing done.
% 201.56/31.16 % (864095)Refutation found. Thanks to Tanya!
% 201.56/31.16 % SZS status Theorem for theBenchmark
% 201.56/31.16 % SZS output start Proof for theBenchmark
% See solution above
% 201.56/31.16 % (864095)------------------------------
% 201.56/31.16 % (864095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.56/31.16 % (864095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.56/31.16 % (864095)CaDiCaL version: 2.1.3
% 201.56/31.16 % (864095)Termination reason: Refutation
% 201.56/31.16 % (864095)Time elapsed: 27.573 s
% 201.56/31.16 % (864095)Peak memory usage: 724 MB
% 201.56/31.16 % (864095)Instructions burned: 55633 (million)
% 201.56/31.16 % (864089)Success in time 30.727 s
% 201.56/31.16 % Vampire exiting
%------------------------------------------------------------------------------