%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR083+4 : 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 : n026.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:03 AM UTC 2026
% Result : Theorem 67.99s 10.05s
% Output : Refutation 67.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 12
% Syntax : Number of formulae : 52 ( 20 unt; 2 def)
% Number of atoms : 117 ( 4 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 121 ( 56 ~; 51 |; 9 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 38 ( 0 sgn 36 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f1291,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__subclass(X1,X2) )
=> s__subclass(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_1294) ).
fof(f5923,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5997) ).
fof(f5956,axiom,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6030) ).
fof(f5972,axiom,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6046) ).
fof(f5999,axiom,
s__subclass(s__Primate,s__Mammal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6073) ).
fof(f6009,axiom,
s__subclass(s__Hominid,s__Primate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6083) ).
fof(f6012,axiom,
s__subclass(s__Human,s__Hominid),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6086) ).
fof(f6013,axiom,
s__subclass(s__Human,s__CognitiveAgent),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6087) ).
fof(f7218,conjecture,
? [X0] :
( s__subclass(X0,s__Animal)
& s__subclass(X0,s__CognitiveAgent)
& X0 = s__Human ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7219,negated_conjecture,
~ ? [X0] :
( s__subclass(X0,s__Animal)
& s__subclass(X0,s__CognitiveAgent)
& X0 = s__Human ),
inference(negated_conjecture,[status(cth)],[f7218]) ).
fof(f7313,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f8537,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f1291]) ).
fof(f8538,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f8537]) ).
fof(f12407,plain,
! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__subclass(X0,s__CognitiveAgent)
| s__Human != X0 ),
inference(ennf_transformation,[],[f7219]) ).
fof(f14333,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7313]) ).
fof(f14334,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f7313]) ).
fof(f15752,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f8538]) ).
fof(f21052,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f5923]) ).
fof(f21085,plain,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f5956]) ).
fof(f21103,plain,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f5972]) ).
fof(f21130,plain,
s__subclass(s__Primate,s__Mammal),
inference(cnf_transformation,[],[f5999]) ).
fof(f21140,plain,
s__subclass(s__Hominid,s__Primate),
inference(cnf_transformation,[],[f6009]) ).
fof(f21143,plain,
s__subclass(s__Human,s__Hominid),
inference(cnf_transformation,[],[f6012]) ).
fof(f21144,plain,
s__subclass(s__Human,s__CognitiveAgent),
inference(cnf_transformation,[],[f6013]) ).
fof(f22555,plain,
! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__subclass(X0,s__CognitiveAgent)
| s__Human != X0 ),
inference(cnf_transformation,[],[f12407]) ).
fof(f22917,plain,
( ~ s__subclass(s__Human,s__Animal)
| ~ s__subclass(s__Human,s__CognitiveAgent) ),
inference(equality_resolution,[],[f22555]) ).
fof(f22946,definition,
( spl504_1
<=> s__subclass(s__Human,s__CognitiveAgent) ),
introduced(definition,[new_symbols(definition,[spl504_1])],[avatar_definition]) ).
fof(f22950,definition,
( spl504_2
<=> s__subclass(s__Human,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl504_2])],[avatar_definition]) ).
fof(f22952,plain,
( ~ s__subclass(s__Human,s__Animal)
| spl504_2 ),
inference(avatar_component_clause,[],[f22950]) ).
fof(f22953,plain,
( ~ spl504_1
| ~ spl504_2 ),
inference(avatar_split_clause,[],[f22917,f22950,f22946]) ).
fof(f22992,plain,
spl504_1,
inference(avatar_split_clause,[],[f21144,f22946]) ).
fof(f44850,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f15752,f14333]) ).
fof(f45058,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f44850,f14333]) ).
fof(f45080,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2) ),
inference(forward_subsumption_resolution,[],[f45058,f14334]) ).
fof(f106461,plain,
( ! [X0] :
( ~ s__subclass(s__Human,X0)
| ~ s__subclass(X0,s__Animal) )
| spl504_2 ),
inference(resolution,[],[f45080,f22952]) ).
fof(f106465,plain,
( ~ s__subclass(s__Human,s__Vertebrate)
| spl504_2 ),
inference(resolution,[],[f106461,f21052]) ).
fof(f106467,plain,
( ! [X0] :
( ~ s__subclass(s__Human,X0)
| ~ s__subclass(X0,s__Vertebrate) )
| spl504_2 ),
inference(resolution,[],[f106465,f45080]) ).
fof(f106473,plain,
( ~ s__subclass(s__Human,s__WarmBloodedVertebrate)
| spl504_2 ),
inference(resolution,[],[f106467,f21085]) ).
fof(f106475,plain,
( ! [X0] :
( ~ s__subclass(s__Human,X0)
| ~ s__subclass(X0,s__WarmBloodedVertebrate) )
| spl504_2 ),
inference(resolution,[],[f106473,f45080]) ).
fof(f106506,plain,
( ~ s__subclass(s__Human,s__Mammal)
| spl504_2 ),
inference(resolution,[],[f106475,f21103]) ).
fof(f106516,plain,
( ! [X0] :
( ~ s__subclass(s__Human,X0)
| ~ s__subclass(X0,s__Mammal) )
| spl504_2 ),
inference(resolution,[],[f106506,f45080]) ).
fof(f106553,plain,
( ~ s__subclass(s__Human,s__Primate)
| spl504_2 ),
inference(resolution,[],[f106516,f21130]) ).
fof(f106559,plain,
( ! [X0] :
( ~ s__subclass(s__Human,X0)
| ~ s__subclass(X0,s__Primate) )
| spl504_2 ),
inference(resolution,[],[f106553,f45080]) ).
fof(f106592,plain,
( ~ s__subclass(s__Human,s__Hominid)
| spl504_2 ),
inference(resolution,[],[f106559,f21140]) ).
fof(f106593,plain,
( $false
| spl504_2 ),
inference(forward_subsumption_resolution,[],[f106592,f21143]) ).
fof(f106594,plain,
spl504_2,
inference(avatar_contradiction_clause,[],[f106593]) ).
cnf(s1,plain,
( ~ spl504_1
| ~ spl504_2 ),
inference(sat_conversion,[],[f22953]) ).
cnf(s8,plain,
spl504_1,
inference(sat_conversion,[],[f22992]) ).
cnf(s11893,plain,
spl504_2,
inference(sat_conversion,[],[f106594]) ).
cnf(s12123,plain,
$false,
inference(rat,[],[s1,s11893,s8]) ).
fof(f106595,plain,
$false,
inference(avatar_sat_refutation,[],[s12123]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR083+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 22:35:42 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 7.14/1.69 % (165656)Will run a generic schedule for satisfiability detection.
% 7.14/1.69 % (165664)dis+10_1_sil=32000:sp=arity:random_seed=439599713:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.14/1.69 % (165662)% WARNING: option uhcvi not known.
% 7.14/1.69 % (165661)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3988644481_2998 on theBenchmark for (2998ds/0Mi)
% 7.14/1.69 % (165662)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2741861853:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.14/1.69 % (165663)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=824224966:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.14/1.69 % (165665)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=27049231:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.14/1.69 % (165667)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=128370477:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.14/1.69 % (165666)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3200970029:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.14/1.69 % (165664)Instruction limit reached!
% 7.14/1.69 % (165664)------------------------------
% 7.14/1.69 % (165664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.69 % (165664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.69 % (165664)CaDiCaL version: 2.1.3
% 7.14/1.69 % (165664)Termination reason: Instruction limit
% 7.14/1.69 % (165664)Termination phase: Property scanning
% 7.14/1.69 % (165664)Time elapsed: 0.038 s
% 7.14/1.69 % (165664)Peak memory usage: 24 MB
% 7.14/1.69 % (165664)Instructions burned: 105 (million)
% 7.14/1.69 % (165675)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2195732422:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 7.14/1.69 % (165665)Instruction limit reached!
% 7.14/1.69 % (165665)------------------------------
% 7.14/1.69 % (165665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.69 % (165665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.69 % (165665)CaDiCaL version: 2.1.3
% 7.14/1.70 % (165665)Termination reason: Instruction limit
% 7.14/1.70 % (165665)Termination phase: Property scanning
% 7.14/1.70 % (165665)Time elapsed: 0.075 s
% 7.14/1.70 % (165665)Peak memory usage: 26 MB
% 7.14/1.70 % (165665)Instructions burned: 116 (million)
% 7.14/1.70 % (165666)Instruction limit reached!
% 7.14/1.70 % (165666)------------------------------
% 7.14/1.70 % (165666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.70 % (165666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.70 % (165666)CaDiCaL version: 2.1.3
% 7.14/1.70 % (165666)Termination reason: Instruction limit
% 7.14/1.70 % (165666)Termination phase: Property scanning
% 7.14/1.70 % (165666)Time elapsed: 0.082 s
% 7.14/1.70 % (165666)Peak memory usage: 24 MB
% 7.14/1.70 % (165666)Instructions burned: 131 (million)
% 7.14/1.70 % (165667)Instruction limit reached!
% 7.14/1.70 % (165667)------------------------------
% 7.14/1.70 % (165667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.70 % (165667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.70 % (165667)CaDiCaL version: 2.1.3
% 7.14/1.70 % (165667)Termination reason: Instruction limit
% 7.14/1.70 % (165667)Termination phase: Property scanning
% 7.14/1.70 % (165667)Time elapsed: 0.092 s
% 7.14/1.70 % (165667)Peak memory usage: 25 MB
% 7.14/1.70 % (165667)Instructions burned: 160 (million)
% 7.14/1.70 % (165677)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1657801604:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.14/1.70 % (165678)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=936159021:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 7.14/1.70 % (165679)ott-21_1_sil=16000:fs=off:random_seed=3999170218:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 7.14/1.70 % (165677)Instruction limit reached!
% 7.14/1.70 % (165677)------------------------------
% 7.14/1.70 % (165677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.70 % (165677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.70 % (165677)CaDiCaL version: 2.1.3
% 7.14/1.70 % (165677)Termination reason: Instruction limit
% 15.41/2.77 % (165677)Termination phase: Property scanning
% 15.41/2.77 % (165677)Time elapsed: 0.080 s
% 15.41/2.77 % (165677)Peak memory usage: 25 MB
% 15.41/2.77 % (165677)Instructions burned: 133 (million)
% 15.41/2.77 % (165683)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3213043888:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 15.41/2.77 % (165679)Instruction limit reached!
% 15.41/2.77 % (165679)------------------------------
% 15.41/2.77 % (165679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165679)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165679)Termination reason: Instruction limit
% 15.41/2.77 % (165679)Termination phase: Property scanning
% 15.41/2.77 % (165679)Time elapsed: 0.098 s
% 15.41/2.77 % (165679)Peak memory usage: 25 MB
% 15.41/2.77 % (165679)Instructions burned: 181 (million)
% 15.41/2.77 % (165685)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3973834966:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 15.41/2.77 % (165675)Instruction limit reached!
% 15.41/2.77 % (165675)------------------------------
% 15.41/2.77 % (165675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165675)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165675)Termination reason: Instruction limit
% 15.41/2.77 % (165675)Termination phase: Finite model building preprocessing
% 15.41/2.77 % (165675)Time elapsed: 0.190 s
% 15.41/2.77 % (165675)Peak memory usage: 36 MB
% 15.41/2.77 % (165675)Instructions burned: 719 (million)
% 15.41/2.77 % (165687)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1453813199:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 15.41/2.77 % (165683)Instruction limit reached!
% 15.41/2.77 % (165683)------------------------------
% 15.41/2.77 % (165683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165683)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165683)Termination reason: Instruction limit
% 15.41/2.77 % (165683)Termination phase: Saturation
% 15.41/2.77 % (165683)Time elapsed: 0.253 s
% 15.41/2.77 % (165683)Peak memory usage: 30 MB
% 15.41/2.77 % (165683)Instructions burned: 477 (million)
% 15.41/2.77 % (165689)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2075624246:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 15.41/2.77 % (165678)Instruction limit reached!
% 15.41/2.77 % (165678)------------------------------
% 15.41/2.77 % (165678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165678)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165678)Termination reason: Instruction limit
% 15.41/2.77 % (165678)Termination phase: Saturation
% 15.41/2.77 % (165678)Time elapsed: 0.372 s
% 15.41/2.77 % (165678)Peak memory usage: 34 MB
% 15.41/2.77 % (165678)Instructions burned: 685 (million)
% 15.41/2.77 % (165691)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=650572698: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)
% 15.41/2.77 % (165687)Instruction limit reached!
% 15.41/2.77 % (165687)------------------------------
% 15.41/2.77 % (165687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165687)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165687)Termination reason: Instruction limit
% 15.41/2.77 % (165687)Termination phase: Saturation
% 15.41/2.77 % (165687)Time elapsed: 0.323 s
% 15.41/2.77 % (165687)Peak memory usage: 36 MB
% 15.41/2.77 % (165687)Instructions burned: 1182 (million)
% 15.41/2.77 % (165693)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=734511377:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 15.41/2.77 % (165685)Instruction limit reached!
% 15.41/2.77 % (165685)------------------------------
% 15.41/2.77 % (165685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.41/2.77 % (165685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.41/2.77 % (165685)CaDiCaL version: 2.1.3
% 15.41/2.77 % (165685)Termination reason: Instruction limit
% 15.41/2.77 % (165685)Termination phase: Finite model building preprocessing
% 27.46/4.37 % (165685)Time elapsed: 0.417 s
% 27.46/4.37 % (165685)Peak memory usage: 39 MB
% 27.46/4.37 % (165685)Instructions burned: 867 (million)
% 27.46/4.37 % (165695)fmb+10_1_sil=64000:random_seed=45288573:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 27.46/4.37 % Detected minimum model sizes of [51]
% 27.46/4.37 % Detected maximum model sizes of [max]
% 27.46/4.37 % (165661)Cannot represent all propositional literals internally
% 27.46/4.37 % (165661)Refutation not found, incomplete strategy
% 27.46/4.37 % (165661)------------------------------
% 27.46/4.37 % (165661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.46/4.37 % (165661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/4.37 % (165661)CaDiCaL version: 2.1.3
% 27.46/4.37 % (165661)Termination reason: Refutation not found, incomplete strategy
% 27.46/4.37 % (165661)Time elapsed: 0.706 s
% 27.46/4.37 % (165661)Peak memory usage: 48 MB
% 27.46/4.37 % (165661)Instructions burned: 1465 (million)
% 27.46/4.37 % (165661)------------------------------
% 27.46/4.37 % (165661)------------------------------
% 27.46/4.37 % (165697)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2252755302:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 27.46/4.37 % (165693)Instruction limit reached!
% 27.46/4.37 % (165693)------------------------------
% 27.46/4.37 % (165693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.46/4.37 % (165693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/4.37 % (165693)CaDiCaL version: 2.1.3
% 27.46/4.37 % (165693)Termination reason: Instruction limit
% 27.46/4.37 % (165693)Termination phase: Saturation
% 27.46/4.37 % (165693)Time elapsed: 0.228 s
% 27.46/4.37 % (165693)Peak memory usage: 38 MB
% 27.46/4.37 % (165693)Instructions burned: 883 (million)
% 27.46/4.37 % (165699)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=353696743:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 27.46/4.37 % (165691)Instruction limit reached!
% 27.46/4.37 % (165691)------------------------------
% 27.46/4.37 % (165691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.46/4.37 % (165691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/4.37 % (165691)CaDiCaL version: 2.1.3
% 27.46/4.37 % (165691)Termination reason: Instruction limit
% 27.46/4.37 % (165691)Termination phase: Saturation
% 27.46/4.37 % (165691)Time elapsed: 0.386 s
% 27.46/4.37 % (165691)Peak memory usage: 35 MB
% 27.46/4.37 % (165691)Instructions burned: 693 (million)
% 27.46/4.37 % (165701)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=400030778:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 27.46/4.37 % (165689)Instruction limit reached!
% 27.46/4.37 % (165689)------------------------------
% 27.46/4.37 % (165689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.46/4.37 % (165689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/4.37 % (165689)CaDiCaL version: 2.1.3
% 27.46/4.37 % (165689)Termination reason: Instruction limit
% 27.46/4.37 % (165689)Termination phase: Finite model building preprocessing
% 27.46/4.37 % (165689)Time elapsed: 0.451 s
% 27.46/4.37 % (165689)Peak memory usage: 40 MB
% 27.46/4.37 % (165689)Instructions burned: 891 (million)
% 27.46/4.37 % (165703)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=877990065:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 27.46/4.37 % (165699)Instruction limit reached!
% 27.46/4.37 % (165699)------------------------------
% 27.46/4.37 % (165699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.46/4.37 % (165699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/4.37 % (165699)CaDiCaL version: 2.1.3
% 27.46/4.37 % (165699)Termination reason: Instruction limit
% 27.46/4.37 % (165699)Termination phase: Finite model building preprocessing
% 27.46/4.37 % (165699)Time elapsed: 0.240 s
% 27.46/4.37 % (165699)Peak memory usage: 39 MB
% 27.46/4.37 % (165699)Instructions burned: 923 (million)
% 27.46/4.37 % (165705)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4005424388:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 27.46/4.37 % Detected minimum model sizes of [51]
% 27.46/4.37 % Detected maximum model sizes of [max]
% 27.46/4.37 % (165695)Cannot represent all propositional literals internally
% 27.46/4.37 % (165695)Refutation not found, incomplete strategy
% 27.46/4.37 % (165695)------------------------------
% 27.46/4.37 % (165695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165695)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165695)Termination reason: Refutation not found, incomplete strategy
% 35.67/5.70 % (165695)Time elapsed: 0.556 s
% 35.67/5.70 % (165695)Peak memory usage: 42 MB
% 35.67/5.70 % (165695)Instructions burned: 1181 (million)
% 35.67/5.70 % (165695)------------------------------
% 35.67/5.70 % (165695)------------------------------
% 35.67/5.70 % (165707)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=829317804:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 35.67/5.70 % Detected minimum model sizes of [51]
% 35.67/5.70 % Detected maximum model sizes of [max]
% 35.67/5.70 % (165697)Cannot represent all propositional literals internally
% 35.67/5.70 % (165697)Refutation not found, incomplete strategy
% 35.67/5.70 % (165697)------------------------------
% 35.67/5.70 % (165697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165697)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165697)Termination reason: Refutation not found, incomplete strategy
% 35.67/5.70 % (165697)Time elapsed: 0.591 s
% 35.67/5.70 % (165697)Peak memory usage: 44 MB
% 35.67/5.70 % (165697)Instructions burned: 1256 (million)
% 35.67/5.70 % (165697)------------------------------
% 35.67/5.70 % (165697)------------------------------
% 35.67/5.70 % (165709)ott-2_1_sil=16000:newcnf=on:random_seed=915689915:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi)
% 35.67/5.70 % Detected minimum model sizes of [51]
% 35.67/5.70 % Detected maximum model sizes of [max]
% 35.67/5.70 % (165705)Cannot represent all propositional literals internally
% 35.67/5.70 % (165705)Refutation not found, incomplete strategy
% 35.67/5.70 % (165705)------------------------------
% 35.67/5.70 % (165705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165705)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165705)Termination reason: Refutation not found, incomplete strategy
% 35.67/5.70 % (165705)Time elapsed: 0.384 s
% 35.67/5.70 % (165705)Peak memory usage: 48 MB
% 35.67/5.70 % (165705)Instructions burned: 1456 (million)
% 35.67/5.70 % (165705)------------------------------
% 35.67/5.70 % (165705)------------------------------
% 35.67/5.70 % (165711)ott+10_1_sil=32000:tgt=ground:random_seed=1464086469:i=5114:av=off_2983 on theBenchmark for (2983ds/5114Mi)
% 35.67/5.70 % (165703)Instruction limit reached!
% 35.67/5.70 % (165703)------------------------------
% 35.67/5.70 % (165703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165703)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165703)Termination reason: Instruction limit
% 35.67/5.70 % (165703)Termination phase: Saturation
% 35.67/5.70 % (165703)Time elapsed: 0.759 s
% 35.67/5.70 % (165703)Peak memory usage: 44 MB
% 35.67/5.70 % (165703)Instructions burned: 1473 (million)
% 35.67/5.70 % (165713)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=995413549:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 35.67/5.70 % (165709)Instruction limit reached!
% 35.67/5.70 % (165709)------------------------------
% 35.67/5.70 % (165709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165709)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165709)Termination reason: Instruction limit
% 35.67/5.70 % (165709)Termination phase: Saturation
% 35.67/5.70 % (165709)Time elapsed: 0.455 s
% 35.67/5.70 % (165709)Peak memory usage: 38 MB
% 35.67/5.70 % (165709)Instructions burned: 870 (million)
% 35.67/5.70 % (165715)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1814501127:i=3512:aac=none_2979 on theBenchmark for (2979ds/3512Mi)
% 35.67/5.70 % (165707)Instruction limit reached!
% 35.67/5.70 % (165707)------------------------------
% 35.67/5.70 % (165707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.67/5.70 % (165707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.67/5.70 % (165707)CaDiCaL version: 2.1.3
% 35.67/5.70 % (165707)Termination reason: Instruction limit
% 35.67/5.70 % (165707)Termination phase: Finite model building preprocessing
% 35.67/5.70 % (165707)Time elapsed: 1.042 s
% 35.67/5.70 % (165707)Peak memory usage: 62 MB
% 67.28/10.04 % (165707)Instructions burned: 2174 (million)
% 67.28/10.04 % (165717)dis+21_1_sil=32000:sas=cadical:random_seed=1727876955:i=3773:amm=off_2974 on theBenchmark for (2974ds/3773Mi)
% 67.28/10.04 % Detected minimum model sizes of [51]
% 67.28/10.04 % Detected maximum model sizes of [max]
% 67.28/10.04 % (165713)Cannot represent all propositional literals internally
% 67.28/10.04 % (165713)Refutation not found, incomplete strategy
% 67.28/10.04 % (165713)------------------------------
% 67.28/10.04 % (165713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165713)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165713)Termination reason: Refutation not found, incomplete strategy
% 67.28/10.04 % (165713)Time elapsed: 0.700 s
% 67.28/10.04 % (165713)Peak memory usage: 48 MB
% 67.28/10.04 % (165713)Instructions burned: 1461 (million)
% 67.28/10.04 % (165713)------------------------------
% 67.28/10.04 % (165713)------------------------------
% 67.28/10.04 % (165719)ott+11_1_sil=16000:gs=on:random_seed=3955327382:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2973 on theBenchmark for (2973ds/2251Mi)
% 67.28/10.04 % (165711)Instruction limit reached!
% 67.28/10.04 % (165711)------------------------------
% 67.28/10.04 % (165711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165711)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165711)Termination reason: Instruction limit
% 67.28/10.04 % (165711)Termination phase: Saturation
% 67.28/10.04 % (165711)Time elapsed: 1.397 s
% 67.28/10.04 % (165711)Peak memory usage: 63 MB
% 67.28/10.04 % (165711)Instructions burned: 5116 (million)
% 67.28/10.04 % (165721)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3029919070:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi)
% 67.28/10.04 % Detected minimum model sizes of [51]
% 67.28/10.04 % Detected maximum model sizes of [max]
% 67.28/10.04 % (165721)Cannot represent all propositional literals internally
% 67.28/10.04 % (165721)Refutation not found, incomplete strategy
% 67.28/10.04 % (165721)------------------------------
% 67.28/10.04 % (165721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165721)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165721)Termination reason: Refutation not found, incomplete strategy
% 67.28/10.04 % (165721)Time elapsed: 0.360 s
% 67.28/10.04 % (165721)Peak memory usage: 45 MB
% 67.28/10.04 % (165721)Instructions burned: 1417 (million)
% 67.28/10.04 % (165721)------------------------------
% 67.28/10.04 % (165721)------------------------------
% 67.28/10.04 % (165723)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=64090778:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi)
% 67.28/10.04 % (165715)Instruction limit reached!
% 67.28/10.04 % (165715)------------------------------
% 67.28/10.04 % (165715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165715)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165715)Termination reason: Instruction limit
% 67.28/10.04 % (165715)Termination phase: Saturation
% 67.28/10.04 % (165715)Time elapsed: 1.511 s
% 67.28/10.04 % (165715)Peak memory usage: 60 MB
% 67.28/10.04 % (165715)Instructions burned: 3515 (million)
% 67.28/10.04 % (165725)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=96588762:i=29340_2964 on theBenchmark for (2964ds/29340Mi)
% 67.28/10.04 % (165701)Instruction limit reached!
% 67.28/10.04 % (165701)------------------------------
% 67.28/10.04 % (165701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165701)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165701)Termination reason: Instruction limit
% 67.28/10.04 % (165701)Termination phase: Saturation
% 67.28/10.04 % (165701)Time elapsed: 2.692 s
% 67.28/10.04 % (165701)Peak memory usage: 57 MB
% 67.28/10.04 % (165701)Instructions burned: 5132 (million)
% 67.28/10.04 % (165727)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3480091337:i=5211_2961 on theBenchmark for (2961ds/5211Mi)
% 67.28/10.04 % (165719)Instruction limit reached!
% 67.28/10.04 % (165719)------------------------------
% 67.28/10.04 % (165719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165719)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165719)Termination reason: Instruction limit
% 67.28/10.04 % (165719)Termination phase: Saturation
% 67.28/10.04 % (165719)Time elapsed: 1.436 s
% 67.28/10.04 % (165719)Peak memory usage: 82 MB
% 67.28/10.04 % (165719)Instructions burned: 2251 (million)
% 67.28/10.04 % (165729)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4290608393:i=5497:nm=2_2958 on theBenchmark for (2958ds/5497Mi)
% 67.28/10.04 % (165717)Instruction limit reached!
% 67.28/10.04 % (165717)------------------------------
% 67.28/10.04 % (165717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165717)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165717)Termination reason: Instruction limit
% 67.28/10.04 % (165717)Termination phase: Saturation
% 67.28/10.04 % (165717)Time elapsed: 1.791 s
% 67.28/10.04 % (165717)Peak memory usage: 72 MB
% 67.28/10.04 % (165717)Instructions burned: 3775 (million)
% 67.28/10.04 % (165731)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3161646836:fmbsr=2:i=46332_2956 on theBenchmark for (2956ds/46332Mi)
% 67.28/10.04 % Detected minimum model sizes of [51]
% 67.28/10.04 % Detected maximum model sizes of [max]
% 67.28/10.04 % (165729)Cannot represent all propositional literals internally
% 67.28/10.04 % (165729)Refutation not found, incomplete strategy
% 67.28/10.04 % (165729)------------------------------
% 67.28/10.04 % (165729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165729)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165729)Termination reason: Refutation not found, incomplete strategy
% 67.28/10.04 % (165729)Time elapsed: 0.654 s
% 67.28/10.04 % (165729)Peak memory usage: 45 MB
% 67.28/10.04 % (165729)Instructions burned: 1327 (million)
% 67.28/10.04 % (165729)------------------------------
% 67.28/10.04 % (165729)------------------------------
% 67.28/10.04 % (165733)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1340330321:i=14071_2951 on theBenchmark for (2951ds/14071Mi)
% 67.28/10.04 % (165723)Instruction limit reached!
% 67.28/10.04 % (165723)------------------------------
% 67.28/10.04 % (165723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165723)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165723)Termination reason: Instruction limit
% 67.28/10.04 % (165723)Termination phase: Saturation
% 67.28/10.04 % (165723)Time elapsed: 1.432 s
% 67.28/10.04 % (165723)Peak memory usage: 94 MB
% 67.28/10.04 % (165723)Instructions burned: 4593 (million)
% 67.28/10.04 % (165735)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3536127338:i=22565:add=on:rawr=on_2950 on theBenchmark for (2950ds/22565Mi)
% 67.28/10.04 % Detected minimum model sizes of [51]
% 67.28/10.04 % Detected maximum model sizes of [max]
% 67.28/10.04 % (165731)Cannot represent all propositional literals internally
% 67.28/10.04 % (165731)Refutation not found, incomplete strategy
% 67.28/10.04 % (165731)------------------------------
% 67.28/10.04 % (165731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165731)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165731)Termination reason: Refutation not found, incomplete strategy
% 67.28/10.04 % (165731)Time elapsed: 0.651 s
% 67.28/10.04 % (165731)Peak memory usage: 45 MB
% 67.28/10.04 % (165731)Instructions burned: 1417 (million)
% 67.28/10.04 % (165731)------------------------------
% 67.28/10.04 % (165731)------------------------------
% 67.28/10.04 % (165737)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2590743267:i=8173:av=off_2949 on theBenchmark for (2949ds/8173Mi)
% 67.28/10.04 % Detected minimum model sizes of [51]
% 67.28/10.04 % Detected maximum model sizes of [max]
% 67.28/10.04 % (165733)Cannot represent all propositional literals internally
% 67.28/10.04 % (165733)Refutation not found, incomplete strategy
% 67.28/10.04 % (165733)------------------------------
% 67.28/10.04 % (165733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.28/10.04 % (165733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.28/10.04 % (165733)CaDiCaL version: 2.1.3
% 67.28/10.04 % (165733)Termination reason: Refutation not found, incomplete strategy
% 67.99/10.05 % (165733)Time elapsed: 0.606 s
% 67.99/10.05 % (165733)Peak memory usage: 46 MB
% 67.99/10.05 % (165733)Instructions burned: 1286 (million)
% 67.99/10.05 % (165733)------------------------------
% 67.99/10.05 % (165733)------------------------------
% 67.99/10.05 % (165739)dis+10_16:1_sil=16000:random_seed=3802775762:i=9155:fsr=off_2945 on theBenchmark for (2945ds/9155Mi)
% 67.99/10.05 % (165727)Instruction limit reached!
% 67.99/10.05 % (165727)------------------------------
% 67.99/10.05 % (165727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.99/10.05 % (165727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.99/10.05 % (165727)CaDiCaL version: 2.1.3
% 67.99/10.05 % (165727)Termination reason: Instruction limit
% 67.99/10.05 % (165727)Termination phase: Saturation
% 67.99/10.05 % (165727)Time elapsed: 2.003 s
% 67.99/10.05 % (165727)Peak memory usage: 47 MB
% 67.99/10.05 % (165727)Instructions burned: 5212 (million)
% 67.99/10.05 % (165741)ott-3_8_sil=64000:random_seed=1691854506:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi)
% 67.99/10.05 % (165737)Instruction limit reached!
% 67.99/10.05 % (165737)------------------------------
% 67.99/10.05 % (165737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.99/10.05 % (165737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.99/10.05 % (165737)CaDiCaL version: 2.1.3
% 67.99/10.05 % (165737)Termination reason: Instruction limit
% 67.99/10.05 % (165737)Termination phase: Saturation
% 67.99/10.05 % (165737)Time elapsed: 4.425 s
% 67.99/10.05 % (165737)Peak memory usage: 110 MB
% 67.99/10.05 % (165737)Instructions burned: 8173 (million)
% 67.99/10.05 % (165743)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3219994908:fmbsr=2:i=32576_2905 on theBenchmark for (2905ds/32576Mi)
% 67.99/10.05 % (165741) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-165656-165741"...
% 67.99/10.05 % (165741)...printing done.
% 67.99/10.05 % (165741)Refutation found. Thanks to Tanya!
% 67.99/10.05 % SZS status Theorem for theBenchmark
% 67.99/10.05 % SZS output start Proof for theBenchmark
% See solution above
% 67.99/10.05 % (165741)------------------------------
% 67.99/10.05 % (165741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.99/10.05 % (165741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.99/10.05 % (165741)CaDiCaL version: 2.1.3
% 67.99/10.05 % (165741)Termination reason: Refutation
% 67.99/10.05 % (165741)Time elapsed: 3.801 s
% 67.99/10.05 % (165741)Peak memory usage: 53 MB
% 67.99/10.05 % (165741)Instructions burned: 6416 (million)
% 67.99/10.05 % (165656)Success in time 9.795 s
% 67.99/10.05 % Vampire exiting
%------------------------------------------------------------------------------