%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR201+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:46:27 AM UTC 2026
% Result : Theorem 177.51s 37.92s
% Output : Refutation 177.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 16
% Syntax : Number of formulae : 64 ( 37 unt; 0 def)
% Number of atoms : 105 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 81 ( 40 ~; 33 |; 3 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-1 aty)
% Number of variables : 53 ( 51 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA8) ).
fof(f3,axiom,
! [X0,X1] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA9) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA15) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA178) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA324) ).
fof(f1582,axiom,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2309) ).
fof(f1585,axiom,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2312) ).
fof(f1591,axiom,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2318) ).
fof(f1607,axiom,
p__d__subclass(c__Replication,c__OrganismProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2336) ).
fof(f1610,axiom,
p__d__subclass(c__SexualReproduction,c__Replication),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2339) ).
fof(f1611,axiom,
p__d__disjoint(c__SexualReproduction,c__AsexualReproduction),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2340) ).
fof(f1613,axiom,
p__d__subclass(c__AsexualReproduction,c__Replication),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2342) ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2644) ).
fof(f7433,conjecture,
~ p__d__subclass(c__Replication,c__SexualReproduction),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',negatedSubclassEvent0127) ).
fof(f7434,negated_conjecture,
~ ~ p__d__subclass(c__Replication,c__SexualReproduction),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7440,plain,
p__d__subclass(c__Replication,c__SexualReproduction),
inference(flattening,[],[f7434]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7451,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7450]) ).
fof(f7452,plain,
! [X0,X1] :
( X0 = X1
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f7453,plain,
! [X0,X1] :
( X0 = X1
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X0) ),
inference(flattening,[],[f7452]) ).
fof(f7454,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7455,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7454]) ).
fof(f7504,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f11602,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7451]) ).
fof(f11603,plain,
! [X0,X1] :
( ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f7453]) ).
fof(f11604,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2) ),
inference(cnf_transformation,[],[f7455]) ).
fof(f11605,plain,
! [X2,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f11883,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| p__d__instance(sK34(X0),X0) ),
inference(cnf_transformation,[],[f7504]) ).
fof(f11886,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f12045,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f13647,plain,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
inference(cnf_transformation,[],[f1582]) ).
fof(f13651,plain,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
inference(cnf_transformation,[],[f1585]) ).
fof(f13659,plain,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
inference(cnf_transformation,[],[f1591]) ).
fof(f13679,plain,
p__d__subclass(c__Replication,c__OrganismProcess),
inference(cnf_transformation,[],[f1607]) ).
fof(f13683,plain,
p__d__subclass(c__SexualReproduction,c__Replication),
inference(cnf_transformation,[],[f1610]) ).
fof(f13684,plain,
p__d__disjoint(c__SexualReproduction,c__AsexualReproduction),
inference(cnf_transformation,[],[f1611]) ).
fof(f13689,plain,
p__d__subclass(c__AsexualReproduction,c__Replication),
inference(cnf_transformation,[],[f1613]) ).
fof(f14072,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[],[f1859]) ).
fof(f22366,plain,
p__d__subclass(c__Replication,c__SexualReproduction),
inference(cnf_transformation,[],[f7440]) ).
fof(f33247,plain,
( ~ p__d__subclass(c__Replication,c__SexualReproduction)
| c__Replication = c__SexualReproduction ),
inference(resolution,[],[f11603,f13683]) ).
fof(f55316,plain,
c__Replication = c__SexualReproduction,
inference(forward_subsumption_resolution,[],[f33247,f22366]) ).
fof(f60505,plain,
! [X0] :
( ~ p__d__instance(X0,c__SexualReproduction)
| ~ p__d__instance(X0,c__AsexualReproduction) ),
inference(resolution,[],[f11605,f13684]) ).
fof(f60617,plain,
p__d__subclass(c__SexualReproduction,c__OrganismProcess),
inference(superposition,[],[f13679,f55316]) ).
fof(f60620,plain,
p__d__subclass(c__AsexualReproduction,c__SexualReproduction),
inference(superposition,[],[f13689,f55316]) ).
fof(f60633,plain,
! [X0] :
( ~ p__d__subclass(c__OrganismProcess,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f60617,f11602]) ).
fof(f60665,plain,
! [X0] :
( ~ p__d__instance(X0,c__AsexualReproduction)
| p__d__instance(X0,c__SexualReproduction) ),
inference(resolution,[],[f60620,f11604]) ).
fof(f60667,plain,
! [X0] :
( ~ p__d__subclass(c__SexualReproduction,X0)
| p__d__subclass(c__AsexualReproduction,X0) ),
inference(resolution,[],[f60620,f11602]) ).
fof(f60891,plain,
p__d__subclass(c__SexualReproduction,c__PhysiologicProcess),
inference(resolution,[],[f60633,f13659]) ).
fof(f60896,plain,
! [X0] :
( ~ p__d__subclass(c__PhysiologicProcess,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f60891,f11602]) ).
fof(f60988,plain,
p__d__subclass(c__SexualReproduction,c__BiologicalProcess),
inference(resolution,[],[f60896,f13651]) ).
fof(f61005,plain,
! [X0] :
( ~ p__d__subclass(c__BiologicalProcess,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f60988,f11602]) ).
fof(f61063,plain,
p__d__subclass(c__SexualReproduction,c__InternalChange),
inference(resolution,[],[f61005,f13647]) ).
fof(f61069,plain,
! [X0] :
( ~ p__d__subclass(c__InternalChange,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f61063,f11602]) ).
fof(f61123,plain,
p__d__subclass(c__SexualReproduction,c__Process),
inference(resolution,[],[f61069,f14072]) ).
fof(f61139,plain,
! [X0] :
( ~ p__d__subclass(c__Process,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f61123,f11602]) ).
fof(f61187,plain,
p__d__subclass(c__SexualReproduction,c__Physical),
inference(resolution,[],[f61139,f12045]) ).
fof(f63889,plain,
! [X0] :
( ~ p__d__subclass(c__Physical,X0)
| p__d__subclass(c__SexualReproduction,X0) ),
inference(resolution,[],[f61187,f11602]) ).
fof(f63958,plain,
p__d__subclass(c__SexualReproduction,c__Entity),
inference(resolution,[],[f63889,f11886]) ).
fof(f63961,plain,
p__d__subclass(c__AsexualReproduction,c__Entity),
inference(resolution,[],[f63958,f60667]) ).
fof(f63979,plain,
p__d__instance(sK34(c__AsexualReproduction),c__AsexualReproduction),
inference(resolution,[],[f63961,f11883]) ).
fof(f392427,plain,
! [X0] : ~ p__d__instance(X0,c__AsexualReproduction),
inference(forward_subsumption_resolution,[],[f60505,f60665]) ).
fof(f392430,plain,
$false,
inference(backward_subsumption_resolution,[],[f63979,f392427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR201+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16 % Computer : n006.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 23:45:55 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.19 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
% 15.41/2.53 % (319442)Will run a generic schedule for satisfiability detection.
% 15.41/2.53 % (319447)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2675505143_2998 on theBenchmark for (2998ds/0Mi)
% 15.41/2.53 % (319448)% WARNING: option uhcvi not known.
% 15.41/2.53 % (319448)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2920745770:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 15.41/2.53 % (319449)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2563623538:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 15.41/2.53 % (319450)dis+10_1_sil=32000:sp=arity:random_seed=3419699924:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 15.41/2.53 % (319451)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2500436573:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 15.41/2.53 % (319452)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2595497411:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 15.41/2.53 % (319453)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2375301007:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 15.41/2.53 % (319450)Instruction limit reached!
% 15.41/2.53 % (319450)------------------------------
% 15.41/2.53 % (319450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.53 % (319450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.53 % (319450)CaDiCaL version: 2.1.3
% 15.41/2.53 % (319450)Termination reason: Instruction limit
% 15.41/2.53 % (319450)Termination phase: Clausification
% 15.41/2.53 % (319450)Time elapsed: 0.065 s
% 15.41/2.53 % (319450)Peak memory usage: 23 MB
% 15.41/2.53 % (319450)Instructions burned: 103 (million)
% 15.41/2.53 % (319451)Instruction limit reached!
% 15.41/2.53 % (319451)------------------------------
% 15.41/2.53 % (319451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.53 % (319451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.53 % (319451)CaDiCaL version: 2.1.3
% 15.41/2.53 % (319451)Termination reason: Instruction limit
% 15.41/2.53 % (319451)Termination phase: NewCNF
% 15.41/2.53 % (319451)Time elapsed: 0.068 s
% 15.41/2.53 % (319451)Peak memory usage: 23 MB
% 15.41/2.53 % (319451)Instructions burned: 116 (million)
% 15.41/2.53 % (319452)Instruction limit reached!
% 15.41/2.53 % (319452)------------------------------
% 15.41/2.53 % (319452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.53 % (319452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.53 % (319452)CaDiCaL version: 2.1.3
% 15.41/2.53 % (319452)Termination reason: Instruction limit
% 15.41/2.53 % (319452)Termination phase: Property scanning
% 15.41/2.53 % (319452)Time elapsed: 0.082 s
% 15.41/2.53 % (319452)Peak memory usage: 24 MB
% 15.41/2.53 % (319452)Instructions burned: 133 (million)
% 15.41/2.53 % (319461)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1097136319:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 15.41/2.53 % (319462)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2192566359:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 15.41/2.53 % (319453)Instruction limit reached!
% 15.41/2.53 % (319453)------------------------------
% 15.41/2.53 % (319453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.53 % (319453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.53 % (319453)CaDiCaL version: 2.1.3
% 15.41/2.53 % (319453)Termination reason: Instruction limit
% 15.41/2.53 % (319453)Termination phase: Property scanning
% 15.41/2.53 % (319453)Time elapsed: 0.094 s
% 15.41/2.53 % (319453)Peak memory usage: 24 MB
% 15.41/2.53 % (319453)Instructions burned: 159 (million)
% 15.41/2.53 % (319464)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=2979595826:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 15.41/2.53 % (319466)ott-21_1_sil=16000:fs=off:random_seed=582558635:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 15.41/2.53 % (319462)Instruction limit reached!
% 15.41/2.53 % (319462)------------------------------
% 15.41/2.53 % (319462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.53 % (319462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.53 % (319462)CaDiCaL version: 2.1.3
% 15.41/2.53 % (319462)Termination reason: Instruction limit
% 38.84/5.85 % (319462)Termination phase: Property scanning
% 38.84/5.85 % (319462)Time elapsed: 0.080 s
% 38.84/5.85 % (319462)Peak memory usage: 24 MB
% 38.84/5.85 % (319462)Instructions burned: 132 (million)
% 38.84/5.85 % (319469)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3165865531:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 38.84/5.85 % (319466)Instruction limit reached!
% 38.84/5.85 % (319466)------------------------------
% 38.84/5.85 % (319466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319466)CaDiCaL version: 2.1.3
% 38.84/5.85 % (319466)Termination reason: Instruction limit
% 38.84/5.85 % (319466)Termination phase: Property scanning
% 38.84/5.85 % (319466)Time elapsed: 0.102 s
% 38.84/5.85 % (319466)Peak memory usage: 24 MB
% 38.84/5.85 % (319466)Instructions burned: 183 (million)
% 38.84/5.85 % (319471)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1310532212:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 38.84/5.85 % TRYING [1]
% 38.84/5.85 % TRYING [2]
% 38.84/5.85 % (319461)Instruction limit reached!
% 38.84/5.85 % (319461)------------------------------
% 38.84/5.85 % (319461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319461)CaDiCaL version: 2.1.3
% 38.84/5.85 % (319461)Termination reason: Instruction limit
% 38.84/5.85 % (319461)Termination phase: Finite model building preprocessing
% 38.84/5.85 % (319461)Time elapsed: 0.346 s
% 38.84/5.85 % (319461)Peak memory usage: 37 MB
% 38.84/5.85 % (319461)Instructions burned: 714 (million)
% 38.84/5.85 % (319469)Instruction limit reached!
% 38.84/5.85 % (319469)------------------------------
% 38.84/5.85 % (319469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319469)CaDiCaL version: 2.1.3
% 38.84/5.85 % (319469)Termination reason: Instruction limit
% 38.84/5.85 % (319469)Termination phase: Saturation
% 38.84/5.85 % (319469)Time elapsed: 0.251 s
% 38.84/5.85 % (319469)Peak memory usage: 30 MB
% 38.84/5.85 % (319469)Instructions burned: 478 (million)
% 38.84/5.85 % (319473)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2033808002:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 38.84/5.85 % (319474)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2648315212:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 38.84/5.85 % TRYING [3]
% 38.84/5.85 % (319464)Instruction limit reached!
% 38.84/5.85 % (319464)------------------------------
% 38.84/5.85 % (319464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319464)CaDiCaL version: 2.1.3
% 38.84/5.85 % (319464)Termination reason: Instruction limit
% 38.84/5.85 % (319464)Termination phase: Saturation
% 38.84/5.85 % (319464)Time elapsed: 0.369 s
% 38.84/5.85 % (319464)Peak memory usage: 31 MB
% 38.84/5.85 % (319464)Instructions burned: 685 (million)
% 38.84/5.85 % (319477)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=4047115553:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 38.84/5.85 % (319471)Instruction limit reached!
% 38.84/5.85 % (319471)------------------------------
% 38.84/5.85 % (319471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319471)CaDiCaL version: 2.1.3
% 38.84/5.85 % (319471)Termination reason: Instruction limit
% 38.84/5.85 % (319471)Termination phase: Finite model building preprocessing
% 38.84/5.85 % (319471)Time elapsed: 0.423 s
% 38.84/5.85 % (319471)Peak memory usage: 42 MB
% 38.84/5.85 % (319471)Instructions burned: 866 (million)
% 38.84/5.85 % (319479)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3410020424:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 38.84/5.85 % TRYING [4]
% 38.84/5.85 % (319477)Instruction limit reached!
% 38.84/5.85 % (319477)------------------------------
% 38.84/5.85 % (319477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.84/5.85 % (319477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.84/5.85 % (319477)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319477)Termination reason: Instruction limit
% 91.31/13.22 % (319477)Termination phase: Saturation
% 91.31/13.22 % (319477)Time elapsed: 0.380 s
% 91.31/13.22 % (319477)Peak memory usage: 35 MB
% 91.31/13.22 % (319477)Instructions burned: 693 (million)
% 91.31/13.22 % (319474)Instruction limit reached!
% 91.31/13.22 % (319474)------------------------------
% 91.31/13.22 % (319474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.22 % (319474)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319474)Termination reason: Instruction limit
% 91.31/13.22 % (319474)Termination phase: Finite model building preprocessing
% 91.31/13.22 % (319474)Time elapsed: 0.431 s
% 91.31/13.22 % (319474)Peak memory usage: 40 MB
% 91.31/13.22 % (319474)Instructions burned: 890 (million)
% 91.31/13.22 % (319481)fmb+10_1_sil=64000:random_seed=1530836953:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 91.31/13.22 % (319482)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1686285280:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 91.31/13.22 % (319473)Instruction limit reached!
% 91.31/13.22 % (319473)------------------------------
% 91.31/13.22 % (319473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.22 % (319473)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319473)Termination reason: Instruction limit
% 91.31/13.22 % (319473)Termination phase: Saturation
% 91.31/13.22 % (319473)Time elapsed: 0.611 s
% 91.31/13.22 % (319473)Peak memory usage: 34 MB
% 91.31/13.22 % (319473)Instructions burned: 1180 (million)
% 91.31/13.22 % (319485)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3747716703:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 91.31/13.22 % (319479)Instruction limit reached!
% 91.31/13.22 % (319479)------------------------------
% 91.31/13.22 % (319479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.22 % (319479)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319479)Termination reason: Instruction limit
% 91.31/13.22 % (319479)Termination phase: Saturation
% 91.31/13.22 % (319479)Time elapsed: 0.406 s
% 91.31/13.22 % (319479)Peak memory usage: 38 MB
% 91.31/13.22 % (319479)Instructions burned: 881 (million)
% 91.31/13.22 % (319487)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1392677594:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 91.31/13.22 % TRYING [1]
% 91.31/13.22 % (319482)Cannot represent all propositional literals internally
% 91.31/13.22 % (319482)Refutation not found, incomplete strategy
% 91.31/13.22 % (319482)------------------------------
% 91.31/13.22 % (319482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.22 % (319482)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319482)Termination reason: Refutation not found, incomplete strategy
% 91.31/13.22 % (319482)Time elapsed: 0.552 s
% 91.31/13.22 % (319482)Peak memory usage: 44 MB
% 91.31/13.22 % (319482)Instructions burned: 1161 (million)
% 91.31/13.22 % (319482)------------------------------
% 91.31/13.22 % (319482)------------------------------
% 91.31/13.22 % (319489)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1997359704:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 91.31/13.22 % TRYING [2]
% 91.31/13.22 % (319485)Instruction limit reached!
% 91.31/13.22 % (319485)------------------------------
% 91.31/13.22 % (319485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.22 % (319485)CaDiCaL version: 2.1.3
% 91.31/13.22 % (319485)Termination reason: Instruction limit
% 91.31/13.22 % (319485)Termination phase: Finite model building preprocessing
% 91.31/13.22 % (319485)Time elapsed: 0.446 s
% 91.31/13.22 % (319485)Peak memory usage: 42 MB
% 91.31/13.22 % (319485)Instructions burned: 920 (million)
% 91.31/13.22 % (319491)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1039255901:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 91.31/13.22 % (319491)Cannot represent all propositional literals internally
% 91.31/13.22 % (319491)Refutation not found, incomplete strategy
% 91.31/13.22 % (319491)------------------------------
% 91.31/13.22 % (319491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.22 % (319491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319491)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319491)Termination reason: Refutation not found, incomplete strategy
% 233.18/33.28 % (319491)Time elapsed: 0.593 s
% 233.18/33.28 % (319491)Peak memory usage: 44 MB
% 233.18/33.28 % (319491)Instructions burned: 1216 (million)
% 233.18/33.28 % (319491)------------------------------
% 233.18/33.28 % (319491)------------------------------
% 233.18/33.28 % (319493)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3002995169:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 233.18/33.28 % (319489)Instruction limit reached!
% 233.18/33.28 % (319489)------------------------------
% 233.18/33.28 % (319489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319489)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319489)Termination reason: Instruction limit
% 233.18/33.28 % (319489)Termination phase: Saturation
% 233.18/33.28 % (319489)Time elapsed: 0.751 s
% 233.18/33.28 % (319489)Peak memory usage: 38 MB
% 233.18/33.28 % (319489)Instructions burned: 1472 (million)
% 233.18/33.28 % (319495)ott-2_1_sil=16000:newcnf=on:random_seed=2870206585:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 233.18/33.28 % TRYING [3]
% 233.18/33.28 % (319495)Instruction limit reached!
% 233.18/33.28 % (319495)------------------------------
% 233.18/33.28 % (319495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319495)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319495)Termination reason: Instruction limit
% 233.18/33.28 % (319495)Termination phase: Saturation
% 233.18/33.28 % (319495)Time elapsed: 0.452 s
% 233.18/33.28 % (319495)Peak memory usage: 35 MB
% 233.18/33.28 % (319495)Instructions burned: 869 (million)
% 233.18/33.28 % (319497)ott+10_1_sil=32000:tgt=ground:random_seed=541486951:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 233.18/33.28 % (319493)Instruction limit reached!
% 233.18/33.28 % (319493)------------------------------
% 233.18/33.28 % (319493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319493)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319493)Termination reason: Instruction limit
% 233.18/33.28 % (319493)Termination phase: Finite model building preprocessing
% 233.18/33.28 % (319493)Time elapsed: 1.062 s
% 233.18/33.28 % (319493)Peak memory usage: 67 MB
% 233.18/33.28 % (319493)Instructions burned: 2174 (million)
% 233.18/33.28 % (319499)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1823493649:i=54282_2965 on theBenchmark for (2965ds/54282Mi)
% 233.18/33.28 % TRYING [5]
% 233.18/33.28 % (319487)Instruction limit reached!
% 233.18/33.28 % (319487)------------------------------
% 233.18/33.28 % (319487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319487)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319487)Termination reason: Instruction limit
% 233.18/33.28 % (319487)Termination phase: Saturation
% 233.18/33.28 % (319487)Time elapsed: 2.659 s
% 233.18/33.28 % (319487)Peak memory usage: 55 MB
% 233.18/33.28 % (319487)Instructions burned: 5131 (million)
% 233.18/33.28 % (319501)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1400017321:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 233.18/33.28 % TRYING [1]
% 233.18/33.28 % TRYING [2]
% 233.18/33.28 % TRYING [3]
% 233.18/33.28 % TRYING [4]
% 233.18/33.28 % (319497)Instruction limit reached!
% 233.18/33.28 % (319497)------------------------------
% 233.18/33.28 % (319497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319497)CaDiCaL version: 2.1.3
% 233.18/33.28 % (319497)Termination reason: Instruction limit
% 233.18/33.28 % (319497)Termination phase: Saturation
% 233.18/33.28 % (319497)Time elapsed: 2.651 s
% 233.18/33.28 % (319497)Peak memory usage: 68 MB
% 233.18/33.28 % (319497)Instructions burned: 5116 (million)
% 233.18/33.28 % (319503)dis+21_1_sil=32000:sas=cadical:random_seed=3406281329:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 233.18/33.28 % (319501)Instruction limit reached!
% 233.18/33.28 % (319501)------------------------------
% 233.18/33.28 % (319501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.18/33.28 % (319501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.18/33.28 % (319501)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319501)Termination reason: Instruction limit
% 177.51/37.91 % (319501)Termination phase: Saturation
% 177.51/37.91 % (319501)Time elapsed: 1.669 s
% 177.51/37.91 % (319501)Peak memory usage: 49 MB
% 177.51/37.91 % (319501)Instructions burned: 3514 (million)
% 177.51/37.91 % (319505)ott+11_1_sil=16000:gs=on:random_seed=5133202:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2943 on theBenchmark for (2943ds/2251Mi)
% 177.51/37.91 % TRYING [4]
% 177.51/37.91 % (319505)Instruction limit reached!
% 177.51/37.91 % (319505)------------------------------
% 177.51/37.91 % (319505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319505)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319505)Termination reason: Instruction limit
% 177.51/37.91 % (319505)Termination phase: Saturation
% 177.51/37.91 % (319505)Time elapsed: 1.278 s
% 177.51/37.91 % (319505)Peak memory usage: 99 MB
% 177.51/37.91 % (319505)Instructions burned: 2252 (million)
% 177.51/37.91 % (319507)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1927997705:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 177.51/37.91 % (319503)Instruction limit reached!
% 177.51/37.91 % (319503)------------------------------
% 177.51/37.91 % (319503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319503)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319503)Termination reason: Instruction limit
% 177.51/37.91 % (319503)Termination phase: Saturation
% 177.51/37.91 % (319503)Time elapsed: 1.870 s
% 177.51/37.91 % (319503)Peak memory usage: 60 MB
% 177.51/37.91 % (319503)Instructions burned: 3775 (million)
% 177.51/37.91 % (319509)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2081917912:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi)
% 177.51/37.91 % (319509)Instruction limit reached!
% 177.51/37.91 % (319509)------------------------------
% 177.51/37.91 % (319509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319509)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319509)Termination reason: Instruction limit
% 177.51/37.91 % (319509)Termination phase: Saturation
% 177.51/37.91 % (319509)Time elapsed: 1.877 s
% 177.51/37.91 % (319509)Peak memory usage: 49 MB
% 177.51/37.91 % (319509)Instructions burned: 4592 (million)
% 177.51/37.91 % (319511)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2886367082:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 177.51/37.91 % TRYING [5]
% 177.51/37.91 % (319481)Instruction limit reached!
% 177.51/37.91 % (319481)------------------------------
% 177.51/37.91 % (319481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319481)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319481)Termination reason: Instruction limit
% 177.51/37.91 % (319481)Termination phase: Finite model building SAT solving
% 177.51/37.91 % (319481)Time elapsed: 9.642 s
% 177.51/37.91 % (319481)Peak memory usage: 370 MB
% 177.51/37.91 % (319481)Instructions burned: 22061 (million)
% 177.51/37.91 % (319513)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=355720157:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 177.51/37.91 % TRYING [7]
% 177.51/37.91 % (319513)Instruction limit reached!
% 177.51/37.91 % (319513)------------------------------
% 177.51/37.91 % (319513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319513)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319513)Termination reason: Instruction limit
% 177.51/37.91 % (319513)Termination phase: Saturation
% 177.51/37.91 % (319513)Time elapsed: 1.644 s
% 177.51/37.91 % (319513)Peak memory usage: 45 MB
% 177.51/37.91 % (319513)Instructions burned: 5212 (million)
% 177.51/37.91 % (319515)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3461298699:i=5497:nm=2_2875 on theBenchmark for (2875ds/5497Mi)
% 177.51/37.91 % (319515)Cannot represent all propositional literals internally
% 177.51/37.91 % (319515)Refutation not found, incomplete strategy
% 177.51/37.91 % (319515)------------------------------
% 177.51/37.91 % (319515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319515)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319515)Termination reason: Refutation not found, incomplete strategy
% 177.51/37.91 % (319515)Time elapsed: 0.560 s
% 177.51/37.91 % (319515)Peak memory usage: 43 MB
% 177.51/37.91 % (319515)Instructions burned: 1051 (million)
% 177.51/37.91 % (319515)------------------------------
% 177.51/37.91 % (319515)------------------------------
% 177.51/37.91 % (319517)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2251632061:fmbsr=2:i=46332_2869 on theBenchmark for (2869ds/46332Mi)
% 177.51/37.91 % (319517)Cannot represent all propositional literals internally
% 177.51/37.91 % (319517)Refutation not found, incomplete strategy
% 177.51/37.91 % (319517)------------------------------
% 177.51/37.91 % (319517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319517)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319517)Termination reason: Refutation not found, incomplete strategy
% 177.51/37.91 % (319517)Time elapsed: 0.649 s
% 177.51/37.91 % (319517)Peak memory usage: 44 MB
% 177.51/37.91 % (319517)Instructions burned: 1350 (million)
% 177.51/37.91 % (319517)------------------------------
% 177.51/37.91 % (319517)------------------------------
% 177.51/37.91 % (319519)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3752473661:i=14071_2862 on theBenchmark for (2862ds/14071Mi)
% 177.51/37.91 % TRYING [12]
% 177.51/37.91 % (319519)Instruction limit reached!
% 177.51/37.91 % (319519)------------------------------
% 177.51/37.91 % (319519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319519)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319519)Termination reason: Instruction limit
% 177.51/37.91 % (319519)Termination phase: Finite model building constraint generation
% 177.51/37.91 % (319519)Time elapsed: 4.952 s
% 177.51/37.91 % (319519)Peak memory usage: 761 MB
% 177.51/37.91 % (319519)Instructions burned: 14074 (million)
% 177.51/37.91 % (319521)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3333248287:i=22565:add=on:rawr=on_2812 on theBenchmark for (2812ds/22565Mi)
% 177.51/37.91 % (319511)Instruction limit reached!
% 177.51/37.91 % (319511)------------------------------
% 177.51/37.91 % (319511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319511)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319511)Termination reason: Instruction limit
% 177.51/37.91 % (319511)Termination phase: Saturation
% 177.51/37.91 % (319511)Time elapsed: 14.424 s
% 177.51/37.91 % (319511)Peak memory usage: 301 MB
% 177.51/37.91 % (319511)Instructions burned: 29340 (million)
% 177.51/37.91 % (319523)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1304249722:i=8173:av=off_2761 on theBenchmark for (2761ds/8173Mi)
% 177.51/37.91 % (319523)Instruction limit reached!
% 177.51/37.91 % (319523)------------------------------
% 177.51/37.91 % (319523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319523)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319523)Termination reason: Instruction limit
% 177.51/37.91 % (319523)Termination phase: Saturation
% 177.51/37.91 % (319523)Time elapsed: 4.755 s
% 177.51/37.91 % (319523)Peak memory usage: 102 MB
% 177.51/37.91 % (319523)Instructions burned: 8173 (million)
% 177.51/37.91 % (319525)dis+10_16:1_sil=16000:random_seed=2617423803:i=9155:fsr=off_2713 on theBenchmark for (2713ds/9155Mi)
% 177.51/37.91 % (319507)Instruction limit reached!
% 177.51/37.91 % (319507)------------------------------
% 177.51/37.91 % (319507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.91 % (319507)CaDiCaL version: 2.1.3
% 177.51/37.91 % (319507)Termination reason: Instruction limit
% 177.51/37.91 % (319507)Termination phase: Finite model building constraint generation
% 177.51/37.91 % (319507)Time elapsed: 24.443 s
% 177.51/37.91 % (319507)Peak memory usage: 3470 MB
% 177.51/37.91 % (319507)Instructions burned: 67536 (million)
% 177.51/37.91 % (319527)ott-3_8_sil=64000:random_seed=199302398:i=20139:bs=on_2680 on theBenchmark for (2680ds/20139Mi)
% 177.51/37.91 % (319521)Instruction limit reached!
% 177.51/37.91 % (319521)------------------------------
% 177.51/37.91 % (319521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.91 % (319521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.92 % (319521)CaDiCaL version: 2.1.3
% 177.51/37.92 % (319521)Termination reason: Instruction limit
% 177.51/37.92 % (319521)Termination phase: Saturation
% 177.51/37.92 % (319521)Time elapsed: 14.260 s
% 177.51/37.92 % (319521)Peak memory usage: 439 MB
% 177.51/37.92 % (319521)Instructions burned: 22566 (million)
% 177.51/37.92 % (319529)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2232602398:fmbsr=2:i=32576_2668 on theBenchmark for (2668ds/32576Mi)
% 177.51/37.92 % (319525)Instruction limit reached!
% 177.51/37.92 % (319525)------------------------------
% 177.51/37.92 % (319525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.92 % (319525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.92 % (319525)CaDiCaL version: 2.1.3
% 177.51/37.92 % (319525)Termination reason: Instruction limit
% 177.51/37.92 % (319525)Termination phase: Saturation
% 177.51/37.92 % (319525)Time elapsed: 4.724 s
% 177.51/37.92 % (319525)Peak memory usage: 98 MB
% 177.51/37.92 % (319525)Instructions burned: 9157 (million)
% 177.51/37.92 % (319531)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=982039835:i=11404_2665 on theBenchmark for (2665ds/11404Mi)
% 177.51/37.92 % TRYING [9]
% 177.51/37.92 % TRYING [6]
% 177.51/37.92 % (319499)Instruction limit reached!
% 177.51/37.92 % (319499)------------------------------
% 177.51/37.92 % (319499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.92 % (319499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.92 % (319499)CaDiCaL version: 2.1.3
% 177.51/37.92 % (319499)Termination reason: Instruction limit
% 177.51/37.92 % (319499)Termination phase: Finite model building SAT solving
% 177.51/37.92 % (319499)Time elapsed: 31.609 s
% 177.51/37.92 % (319499)Peak memory usage: 1760 MB
% 177.51/37.92 % (319499)Instructions burned: 54283 (million)
% 177.51/37.92 % (319533)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3986526057:i=14134_2647 on theBenchmark for (2647ds/14134Mi)
% 177.51/37.92 % (319448) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-319442-319448"...
% 177.51/37.92 % (319448)...printing done.
% 177.51/37.92 % (319448)Refutation found. Thanks to Tanya!
% 177.51/37.92 % SZS status Theorem for theBenchmark
% 177.51/37.92 % SZS output start Proof for theBenchmark
% See solution above
% 177.51/37.92 % (319448)------------------------------
% 177.51/37.92 % (319448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.51/37.92 % (319448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.51/37.92 % (319448)CaDiCaL version: 2.1.3
% 177.51/37.92 % (319448)Termination reason: Refutation
% 177.51/37.92 % (319448)Time elapsed: 37.328 s
% 177.51/37.92 % (319448)Peak memory usage: 181 MB
% 177.51/37.92 % (319448)Instructions burned: 64311 (million)
% 177.51/37.92 % (319442)Success in time 37.706 s
% 177.51/37.92 % Vampire exiting
%------------------------------------------------------------------------------