%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR094+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 : 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:45:10 AM UTC 2026
% Result : Theorem 0.18s 29.30s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 26 ( 12 unt; 0 def)
% Number of atoms : 60 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 64 ( 30 ~; 27 |; 4 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 34 ( 34 !; 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(f26457,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_26636) ).
fof(f127121,axiom,
s__subclass(s__Canine,s__CorpuscularObject),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+5.ax',kb_SUMO_71535) ).
fof(f145102,axiom,
s__instance(s__Rover24_1,s__Canine),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f145103,conjecture,
s__instance(s__Rover24_1,s__CorpuscularObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145104,negated_conjecture,
~ s__instance(s__Rover24_1,s__CorpuscularObject),
inference(negated_conjecture,[status(cth)],[f145103]) ).
fof(f145145,plain,
~ s__instance(s__Rover24_1,s__CorpuscularObject),
inference(flattening,[],[f145104]) ).
fof(f154464,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f154465,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f26457]) ).
fof(f154466,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f154465]) ).
fof(f191274,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f154464]) ).
fof(f191275,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f154464]) ).
fof(f191276,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f154466]) ).
fof(f297087,plain,
s__subclass(s__Canine,s__CorpuscularObject),
inference(cnf_transformation,[],[f127121]) ).
fof(f315067,plain,
s__instance(s__Rover24_1,s__Canine),
inference(cnf_transformation,[],[f145102]) ).
fof(f315068,plain,
~ s__instance(s__Rover24_1,s__CorpuscularObject),
inference(cnf_transformation,[],[f145145]) ).
fof(f329302,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191275]) ).
fof(f329303,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f191274]) ).
fof(f329304,plain,
! [X2,X0,X1] :
( s__instance(X0,s__SetOrClass)
| s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(consistent_polarity_flipping,[],[f191276]) ).
fof(f393003,plain,
~ s__instance(s__Rover24_1,s__Canine),
inference(consistent_polarity_flipping,[],[f315067]) ).
fof(f393004,plain,
s__instance(s__Rover24_1,s__CorpuscularObject),
inference(consistent_polarity_flipping,[],[f315068]) ).
fof(f1279865,plain,
! [X2,X0,X1] :
( s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f329304,f329302]) ).
fof(f1279866,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f1279865,f329303]) ).
fof(f1282719,plain,
! [X0] :
( ~ s__subclass(X0,s__CorpuscularObject)
| s__instance(s__Rover24_1,X0) ),
inference(resolution,[],[f1279866,f393004]) ).
fof(f1283207,plain,
s__instance(s__Rover24_1,s__Canine),
inference(resolution,[],[f1282719,f297087]) ).
fof(f1283564,plain,
$false,
inference(forward_subsumption_resolution,[],[f1283207,f393003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR094+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n006.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:43:40 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.85/6.22 % (292844)Will run a generic schedule for satisfiability detection.
% 23.85/6.22 % (292850)% WARNING: option uhcvi not known.
% 23.85/6.22 % (292849)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=709504370_2972 on theBenchmark for (2972ds/0Mi)
% 23.85/6.22 % (292850)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1431015639:i=135531:add=off:rawr=on_2972 on theBenchmark for (2972ds/135531Mi)
% 23.85/6.22 % (292853)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1610073592:i=116_2972 on theBenchmark for (2972ds/116Mi)
% 23.85/6.22 % (292851)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=278205345:i=88024:add=on:rawr=on_2972 on theBenchmark for (2972ds/88024Mi)
% 23.85/6.22 % (292852)dis+10_1_sil=32000:sp=arity:random_seed=3939945348:i=103:fgj=on_2972 on theBenchmark for (2972ds/103Mi)
% 23.85/6.22 % (292854)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3403465899:i=131_2972 on theBenchmark for (2972ds/131Mi)
% 23.85/6.22 % (292855)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3152597217:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2972 on theBenchmark for (2972ds/159Mi)
% 23.85/6.22 % (292853)Instruction limit reached!
% 23.85/6.22 % (292853)------------------------------
% 23.85/6.22 % (292853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.85/6.22 % (292853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.22 % (292853)CaDiCaL version: 2.1.3
% 23.85/6.22 % (292853)Termination reason: Instruction limit
% 23.85/6.22 % (292853)Termination phase: Preprocessing 1
% 23.85/6.22 % (292853)Time elapsed: 0.054 s
% 23.85/6.22 % (292853)Peak memory usage: 155 MB
% 23.85/6.22 % (292853)Instructions burned: 118 (million)
% 23.85/6.22 % (292852)Instruction limit reached!
% 23.85/6.22 % (292852)------------------------------
% 23.85/6.22 % (292852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.85/6.22 % (292852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.22 % (292852)CaDiCaL version: 2.1.3
% 23.85/6.22 % (292852)Termination reason: Instruction limit
% 23.85/6.22 % (292852)Termination phase: Preprocessing 1
% 23.85/6.22 % (292852)Time elapsed: 0.068 s
% 23.85/6.22 % (292852)Peak memory usage: 155 MB
% 23.85/6.22 % (292852)Instructions burned: 103 (million)
% 23.85/6.22 % (292863)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2168447172:i=714:nm=2_2971 on theBenchmark for (2971ds/714Mi)
% 23.85/6.22 % (292854)Instruction limit reached!
% 23.85/6.22 % (292854)------------------------------
% 23.85/6.22 % (292854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.85/6.22 % (292854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.22 % (292854)CaDiCaL version: 2.1.3
% 23.85/6.22 % (292854)Termination reason: Instruction limit
% 23.85/6.22 % (292854)Termination phase: Preprocessing 1
% 23.85/6.22 % (292854)Time elapsed: 0.087 s
% 23.85/6.22 % (292854)Peak memory usage: 155 MB
% 23.85/6.22 % (292854)Instructions burned: 131 (million)
% 23.85/6.22 % (292865)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2742799501:i=131:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/131Mi)
% 23.85/6.22 % (292855)Instruction limit reached!
% 23.85/6.22 % (292855)------------------------------
% 23.85/6.22 % (292855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.85/6.22 % (292855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.22 % (292855)CaDiCaL version: 2.1.3
% 23.85/6.22 % (292855)Termination reason: Instruction limit
% 23.85/6.22 % (292855)Termination phase: Preprocessing 1
% 23.85/6.22 % (292855)Time elapsed: 0.105 s
% 23.85/6.22 % (292855)Peak memory usage: 155 MB
% 23.85/6.22 % (292855)Instructions burned: 159 (million)
% 23.85/6.22 % (292867)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=2720082830:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2971 on theBenchmark for (2971ds/684Mi)
% 23.85/6.22 % (292868)ott-21_1_sil=16000:fs=off:random_seed=759785512:i=180:av=off:fsr=off_2971 on theBenchmark for (2971ds/180Mi)
% 23.85/6.22 % (292865)Instruction limit reached!
% 23.85/6.22 % (292865)------------------------------
% 23.85/6.22 % (292865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.85/6.22 % (292865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.22 % (292865)CaDiCaL version: 2.1.3
% 23.85/6.22 % (292865)Termination reason: Instruction limit
% 55.76/10.42 % (292865)Termination phase: Preprocessing 1
% 55.76/10.42 % (292865)Time elapsed: 0.083 s
% 55.76/10.42 % (292865)Peak memory usage: 155 MB
% 55.76/10.42 % (292865)Instructions burned: 131 (million)
% 55.76/10.42 % (292871)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1384252711:i=477:bd=all_2970 on theBenchmark for (2970ds/477Mi)
% 55.76/10.42 % (292868)Instruction limit reached!
% 55.76/10.42 % (292868)------------------------------
% 55.76/10.42 % (292868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292868)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292868)Termination reason: Instruction limit
% 55.76/10.42 % (292868)Termination phase: Preprocessing 1
% 55.76/10.42 % (292868)Time elapsed: 0.122 s
% 55.76/10.42 % (292868)Peak memory usage: 155 MB
% 55.76/10.42 % (292868)Instructions burned: 180 (million)
% 55.76/10.42 % (292873)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3248445292:fmbsr=1.3:i=865:ins=25_2969 on theBenchmark for (2969ds/865Mi)
% 55.76/10.42 % (292863)Instruction limit reached!
% 55.76/10.42 % (292863)------------------------------
% 55.76/10.42 % (292863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292863)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292863)Termination reason: Instruction limit
% 55.76/10.42 % (292863)Termination phase: Unused predicate definition removal
% 55.76/10.42 % (292863)Time elapsed: 0.240 s
% 55.76/10.42 % (292863)Peak memory usage: 189 MB
% 55.76/10.42 % (292863)Instructions burned: 716 (million)
% 55.76/10.42 % (292875)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1325206858:i=1179_2969 on theBenchmark for (2969ds/1179Mi)
% 55.76/10.42 % (292867)Instruction limit reached!
% 55.76/10.42 % (292867)------------------------------
% 55.76/10.42 % (292867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292867)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292867)Termination reason: Instruction limit
% 55.76/10.42 % (292867)Termination phase: Preprocessing 1
% 55.76/10.42 % (292867)Time elapsed: 0.380 s
% 55.76/10.42 % (292867)Peak memory usage: 158 MB
% 55.76/10.42 % (292867)Instructions burned: 685 (million)
% 55.76/10.42 % (292877)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3799842475:i=889:ins=1_2967 on theBenchmark for (2967ds/889Mi)
% 55.76/10.42 % (292871)Instruction limit reached!
% 55.76/10.42 % (292871)------------------------------
% 55.76/10.42 % (292871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292871)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292871)Termination reason: Instruction limit
% 55.76/10.42 % (292871)Termination phase: Naming
% 55.76/10.42 % (292871)Time elapsed: 0.362 s
% 55.76/10.42 % (292871)Peak memory usage: 164 MB
% 55.76/10.42 % (292871)Instructions burned: 480 (million)
% 55.76/10.42 % (292879)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=2239466220: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)
% 55.76/10.42 % (292875)Instruction limit reached!
% 55.76/10.42 % (292875)------------------------------
% 55.76/10.42 % (292875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292875)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292875)Termination reason: Instruction limit
% 55.76/10.42 % (292875)Termination phase: Property scanning
% 55.76/10.42 % (292875)Time elapsed: 0.417 s
% 55.76/10.42 % (292875)Peak memory usage: 185 MB
% 55.76/10.42 % (292875)Instructions burned: 1182 (million)
% 55.76/10.42 % (292881)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3925502415:i=879:kws=inv_precedence:fsr=off_2964 on theBenchmark for (2964ds/879Mi)
% 55.76/10.42 % (292873)Instruction limit reached!
% 55.76/10.42 % (292873)------------------------------
% 55.76/10.42 % (292873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.76/10.42 % (292873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.76/10.42 % (292873)CaDiCaL version: 2.1.3
% 55.76/10.42 % (292873)Termination reason: Instruction limit
% 79.18/13.79 % (292873)Termination phase: Preprocessing 2
% 79.18/13.79 % (292873)Time elapsed: 0.535 s
% 79.18/13.79 % (292873)Peak memory usage: 203 MB
% 79.18/13.79 % (292873)Instructions burned: 866 (million)
% 79.18/13.79 % (292883)fmb+10_1_sil=64000:random_seed=2309333175:i=22061:nm=2:gsp=on_2963 on theBenchmark for (2963ds/22061Mi)
% 79.18/13.79 % (292879)Instruction limit reached!
% 79.18/13.79 % (292879)------------------------------
% 79.18/13.79 % (292879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292879)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292879)Termination reason: Instruction limit
% 79.18/13.79 % (292879)Termination phase: Preprocessing 1
% 79.18/13.79 % (292879)Time elapsed: 0.400 s
% 79.18/13.79 % (292879)Peak memory usage: 158 MB
% 79.18/13.79 % (292879)Instructions burned: 692 (million)
% 79.18/13.79 % (292885)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1270561691:i=9515:nm=5_2962 on theBenchmark for (2962ds/9515Mi)
% 79.18/13.79 % (292881)Instruction limit reached!
% 79.18/13.79 % (292881)------------------------------
% 79.18/13.79 % (292881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292881)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292881)Termination reason: Instruction limit
% 79.18/13.79 % (292881)Termination phase: NewCNF
% 79.18/13.79 % (292881)Time elapsed: 0.328 s
% 79.18/13.79 % (292881)Peak memory usage: 178 MB
% 79.18/13.79 % (292881)Instructions burned: 882 (million)
% 79.18/13.79 % (292877)Instruction limit reached!
% 79.18/13.79 % (292877)------------------------------
% 79.18/13.79 % (292877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292877)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292877)Termination reason: Instruction limit
% 79.18/13.79 % (292877)Termination phase: Preprocessing 2
% 79.18/13.79 % (292877)Time elapsed: 0.575 s
% 79.18/13.79 % (292877)Peak memory usage: 194 MB
% 79.18/13.79 % (292877)Instructions burned: 889 (million)
% 79.18/13.79 % (292887)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1849871088:fmbsr=1.7:i=920_2961 on theBenchmark for (2961ds/920Mi)
% 79.18/13.79 % (292889)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3301166412:i=5131_2961 on theBenchmark for (2961ds/5131Mi)
% 79.18/13.79 % (292887)Instruction limit reached!
% 79.18/13.79 % (292887)------------------------------
% 79.18/13.79 % (292887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292887)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292887)Termination reason: Instruction limit
% 79.18/13.79 % (292887)Termination phase: Preprocessing 2
% 79.18/13.79 % (292887)Time elapsed: 0.335 s
% 79.18/13.79 % (292887)Peak memory usage: 197 MB
% 79.18/13.79 % (292887)Instructions burned: 924 (million)
% 79.18/13.79 % (292891)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2574721056:i=1472:ins=7:fdi=8:gsp=on_2957 on theBenchmark for (2957ds/1472Mi)
% 79.18/13.79 % (292891)Instruction limit reached!
% 79.18/13.79 % (292891)------------------------------
% 79.18/13.79 % (292891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292891)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292891)Termination reason: Instruction limit
% 79.18/13.79 % (292891)Termination phase: Property scanning
% 79.18/13.79 % (292891)Time elapsed: 0.484 s
% 79.18/13.79 % (292891)Peak memory usage: 185 MB
% 79.18/13.79 % (292891)Instructions burned: 1472 (million)
% 79.18/13.79 % (292893)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2941409622:i=6324_2952 on theBenchmark for (2952ds/6324Mi)
% 79.18/13.79 % (292889)Instruction limit reached!
% 79.18/13.79 % (292889)------------------------------
% 79.18/13.79 % (292889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.18/13.79 % (292889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.18/13.79 % (292889)CaDiCaL version: 2.1.3
% 79.18/13.79 % (292889)Termination reason: Instruction limit
% 79.18/13.79 % (292889)Termination phase: Saturation
% 79.18/13.79 % (292889)Time elapsed: 2.051 s
% 79.18/13.79 % (292889)Peak memory usage: 200 MB
% 79.18/13.79 % (292889)Instructions burned: 5132 (million)
% 79.18/13.79 % (292895)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1257192993:fmbsr=2.30978:i=2174_2940 on theBenchmark for (2940ds/2174Mi)
% 120.30/19.56 % (292893)Instruction limit reached!
% 120.30/19.56 % (292893)------------------------------
% 120.30/19.56 % (292893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292893)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292893)Termination reason: Instruction limit
% 120.30/19.56 % (292893)Termination phase: Property scanning
% 120.30/19.56 % (292893)Time elapsed: 1.904 s
% 120.30/19.56 % (292893)Peak memory usage: 298 MB
% 120.30/19.56 % (292893)Instructions burned: 6326 (million)
% 120.30/19.56 % (292897)ott-2_1_sil=16000:newcnf=on:random_seed=2684124257:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2933 on theBenchmark for (2933ds/869Mi)
% 120.30/19.56 % (292897)Instruction limit reached!
% 120.30/19.56 % (292897)------------------------------
% 120.30/19.56 % (292897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292897)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292897)Termination reason: Instruction limit
% 120.30/19.56 % (292897)Termination phase: NewCNF
% 120.30/19.56 % (292897)Time elapsed: 0.300 s
% 120.30/19.56 % (292897)Peak memory usage: 178 MB
% 120.30/19.56 % (292897)Instructions burned: 871 (million)
% 120.30/19.56 % (292899)ott+10_1_sil=32000:tgt=ground:random_seed=3358133908:i=5114:av=off_2930 on theBenchmark for (2930ds/5114Mi)
% 120.30/19.56 % (292895)Instruction limit reached!
% 120.30/19.56 % (292895)------------------------------
% 120.30/19.56 % (292895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292895)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292895)Termination reason: Instruction limit
% 120.30/19.56 % (292895)Termination phase: Property scanning
% 120.30/19.56 % (292895)Time elapsed: 1.185 s
% 120.30/19.56 % (292895)Peak memory usage: 241 MB
% 120.30/19.56 % (292895)Instructions burned: 2175 (million)
% 120.30/19.56 % (292901)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1960062004:i=54282_2927 on theBenchmark for (2927ds/54282Mi)
% 120.30/19.56 % (292885)Instruction limit reached!
% 120.30/19.56 % (292885)------------------------------
% 120.30/19.56 % (292885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292885)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292885)Termination reason: Instruction limit
% 120.30/19.56 % (292885)Termination phase: Finite model building preprocessing
% 120.30/19.56 % (292885)Time elapsed: 4.717 s
% 120.30/19.56 % (292885)Peak memory usage: 341 MB
% 120.30/19.56 % (292885)Instructions burned: 9518 (million)
% 120.30/19.56 % (292899)Instruction limit reached!
% 120.30/19.56 % (292899)------------------------------
% 120.30/19.56 % (292899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292899)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292899)Termination reason: Instruction limit
% 120.30/19.56 % (292899)Termination phase: Saturation
% 120.30/19.56 % (292899)Time elapsed: 1.557 s
% 120.30/19.56 % (292899)Peak memory usage: 248 MB
% 120.30/19.56 % (292899)Instructions burned: 5114 (million)
% 120.30/19.56 % (292903)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=349117492:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 120.30/19.56 % (292905)dis+21_1_sil=32000:sas=cadical:random_seed=3222817874:i=3773:amm=off_2914 on theBenchmark for (2914ds/3773Mi)
% 120.30/19.56 % (292905)Instruction limit reached!
% 120.30/19.56 % (292905)------------------------------
% 120.30/19.56 % (292905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 120.30/19.56 % (292905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.30/19.56 % (292905)CaDiCaL version: 2.1.3
% 120.30/19.56 % (292905)Termination reason: Instruction limit
% 120.30/19.56 % (292905)Termination phase: Saturation
% 120.30/19.56 % (292905)Time elapsed: 1.068 s
% 120.30/19.56 % (292905)Peak memory usage: 209 MB
% 120.30/19.56 % (292905)Instructions burned: 3776 (million)
% 120.30/19.56 % (292907)ott+11_1_sil=16000:gs=on:random_seed=579562075:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2903 on theBenchmark for (2903ds/2251Mi)
% 120.30/19.56 % Detected minimum model sizes of [617]
% 120.30/19.56 % Detected maximum model sizes of [max]
% 179.30/28.00 % (292883)Cannot represent all propositional literals internally
% 179.30/28.00 % (292883)Refutation not found, incomplete strategy
% 179.30/28.00 % (292883)------------------------------
% 179.30/28.00 % (292883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292883)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292883)Termination reason: Refutation not found, incomplete strategy
% 179.30/28.00 % (292883)Time elapsed: 6.571 s
% 179.30/28.00 % (292883)Peak memory usage: 388 MB
% 179.30/28.00 % (292883)Instructions burned: 13608 (million)
% 179.30/28.00 % (292903)Instruction limit reached!
% 179.30/28.00 % (292903)------------------------------
% 179.30/28.00 % (292903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292903)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292903)Termination reason: Instruction limit
% 179.30/28.00 % (292903)Termination phase: Saturation
% 179.30/28.00 % (292903)Time elapsed: 1.776 s
% 179.30/28.00 % (292903)Peak memory usage: 204 MB
% 179.30/28.00 % (292903)Instructions burned: 3513 (million)
% 179.30/28.00 % (292909)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=797932269:fmbsr=1.6:i=67534_2896 on theBenchmark for (2896ds/67534Mi)
% 179.30/28.00 % (292907)Instruction limit reached!
% 179.30/28.00 % (292907)------------------------------
% 179.30/28.00 % (292907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292907)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292907)Termination reason: Instruction limit
% 179.30/28.00 % (292907)Termination phase: Property scanning
% 179.30/28.00 % (292907)Time elapsed: 0.737 s
% 179.30/28.00 % (292907)Peak memory usage: 188 MB
% 179.30/28.00 % (292907)Instructions burned: 2254 (million)
% 179.30/28.00 % (292911)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3023323528:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2895 on theBenchmark for (2895ds/4591Mi)
% 179.30/28.00 % (292883)------------------------------
% 179.30/28.00 % (292883)------------------------------
% 179.30/28.00 % (292913)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1811534899:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 179.30/28.00 % Detected minimum model sizes of [617]
% 179.30/28.00 % Detected maximum model sizes of [max]
% 179.30/28.00 % (292849)Cannot represent all propositional literals internally
% 179.30/28.00 % (292849)Refutation not found, incomplete strategy
% 179.30/28.00 % (292849)------------------------------
% 179.30/28.00 % (292849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292849)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292849)Termination reason: Refutation not found, incomplete strategy
% 179.30/28.00 % (292849)Time elapsed: 8.363 s
% 179.30/28.00 % (292849)Peak memory usage: 457 MB
% 179.30/28.00 % (292849)Instructions burned: 17060 (million)
% 179.30/28.00 % (292849)------------------------------
% 179.30/28.00 % (292849)------------------------------
% 179.30/28.00 % (292915)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1939417923:i=5211_2885 on theBenchmark for (2885ds/5211Mi)
% 179.30/28.00 % (292911)Instruction limit reached!
% 179.30/28.00 % (292911)------------------------------
% 179.30/28.00 % (292911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292911)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292911)Termination reason: Instruction limit
% 179.30/28.00 % (292911)Termination phase: Saturation
% 179.30/28.00 % (292911)Time elapsed: 1.371 s
% 179.30/28.00 % (292911)Peak memory usage: 238 MB
% 179.30/28.00 % (292911)Instructions burned: 4595 (million)
% 179.30/28.00 % (292917)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1293588040:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 179.30/28.00 % (292917)Instruction limit reached!
% 179.30/28.00 % (292917)------------------------------
% 179.30/28.00 % (292917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 179.30/28.00 % (292917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.30/28.00 % (292917)CaDiCaL version: 2.1.3
% 179.30/28.00 % (292917)Termination reason: Instruction limit
% 179.30/28.00 % (292917)Termination phase: Property scanning
% 179.30/28.00 % (292917)Time elapsed: 1.717 s
% 164.05/29.09 % (292917)Peak memory usage: 301 MB
% 164.05/29.09 % (292917)Instructions burned: 5499 (million)
% 164.05/29.09 % (292919)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=911140127:fmbsr=2:i=46332_2864 on theBenchmark for (2864ds/46332Mi)
% 164.05/29.09 % (292915)Instruction limit reached!
% 164.05/29.09 % (292915)------------------------------
% 164.05/29.09 % (292915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 164.05/29.09 % (292915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.05/29.09 % (292915)CaDiCaL version: 2.1.3
% 164.05/29.09 % (292915)Termination reason: Instruction limit
% 164.05/29.09 % (292915)Termination phase: Saturation
% 164.05/29.09 % (292915)Time elapsed: 2.565 s
% 164.05/29.09 % (292915)Peak memory usage: 238 MB
% 164.05/29.09 % (292915)Instructions burned: 5211 (million)
% 164.05/29.09 % (292921)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=917335372:i=14071_2859 on theBenchmark for (2859ds/14071Mi)
% 164.05/29.09 % Detected minimum model sizes of [617]
% 164.05/29.09 % Detected maximum model sizes of [max]
% 164.05/29.09 % (292901)Cannot represent all propositional literals internally
% 164.05/29.09 % (292901)Refutation not found, incomplete strategy
% 164.05/29.09 % (292901)------------------------------
% 164.05/29.09 % (292901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 164.05/29.09 % (292901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.05/29.09 % (292901)CaDiCaL version: 2.1.3
% 164.05/29.09 % (292901)Termination reason: Refutation not found, incomplete strategy
% 164.05/29.09 % (292901)Time elapsed: 8.469 s
% 164.05/29.09 % (292901)Peak memory usage: 458 MB
% 164.05/29.09 % (292901)Instructions burned: 17085 (million)
% 164.05/29.09 % (292901)------------------------------
% 164.05/29.09 % (292901)------------------------------
% 164.05/29.09 % (292923)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3616519440:i=22565:add=on:rawr=on_2839 on theBenchmark for (2839ds/22565Mi)
% 164.05/29.09 % Detected minimum model sizes of [617]
% 164.05/29.09 % Detected maximum model sizes of [max]
% 164.05/29.09 % (292919)Cannot represent all propositional literals internally
% 164.05/29.09 % (292919)Refutation not found, incomplete strategy
% 164.05/29.09 % (292919)------------------------------
% 164.05/29.09 % (292919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 164.05/29.09 % (292919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.05/29.09 % (292919)CaDiCaL version: 2.1.3
% 164.05/29.09 % (292919)Termination reason: Refutation not found, incomplete strategy
% 164.05/29.09 % (292919)Time elapsed: 4.035 s
% 164.05/29.09 % (292919)Peak memory usage: 415 MB
% 164.05/29.09 % (292919)Instructions burned: 15711 (million)
% 164.05/29.09 % Detected minimum model sizes of [617]
% 164.05/29.09 % Detected maximum model sizes of [max]
% 164.05/29.09 % (292909)Cannot represent all propositional literals internally
% 164.05/29.09 % (292909)Refutation not found, incomplete strategy
% 164.05/29.09 % (292909)------------------------------
% 164.05/29.09 % (292909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 164.05/29.09 % (292909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.05/29.09 % (292909)CaDiCaL version: 2.1.3
% 164.05/29.09 % (292909)Termination reason: Refutation not found, incomplete strategy
% 164.05/29.09 % (292909)Time elapsed: 7.268 s
% 164.05/29.09 % (292909)Peak memory usage: 415 MB
% 164.05/29.09 % (292909)Instructions burned: 15712 (million)
% 164.05/29.09 % (292919)------------------------------
% 164.05/29.09 % (292919)------------------------------
% 164.05/29.09 % (292925)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3951259249:i=8173:av=off_2821 on theBenchmark for (2821ds/8173Mi)
% 164.05/29.09 % (292909)------------------------------
% 164.05/29.09 % (292909)------------------------------
% 164.05/29.09 % (292927)dis+10_16:1_sil=16000:random_seed=2722557155:i=9155:fsr=off_2820 on theBenchmark for (2820ds/9155Mi)
% 164.05/29.09 % (292925)Instruction limit reached!
% 164.05/29.09 % (292925)------------------------------
% 164.05/29.09 % (292925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 164.05/29.09 % (292925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.05/29.09 % (292925)CaDiCaL version: 2.1.3
% 164.05/29.09 % (292925)Termination reason: Instruction limit
% 164.05/29.09 % (292925)Termination phase: Saturation
% 164.05/29.09 % (292925)Time elapsed: 1.447 s
% 164.05/29.09 % (292925)Peak memory usage: 197 MB
% 164.05/29.09 % (292925)Instructions burned: 8174 (million)
% 164.05/29.09 % (292929)ott-3_8_sil=64000:random_seed=2066831111:i=20139:bs=on_2806 on theBenchmark for (2806ds/20139Mi)
% 0.18/29.30 % (292921)Instruction limit reached!
% 0.18/29.30 % (292921)------------------------------
% 0.18/29.30 % (292921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292921)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292921)Termination reason: Instruction limit
% 0.18/29.30 % (292921)Termination phase: Finite model building preprocessing
% 0.18/29.30 % (292921)Time elapsed: 6.605 s
% 0.18/29.30 % (292921)Peak memory usage: 390 MB
% 0.18/29.30 % (292921)Instructions burned: 14072 (million)
% 0.18/29.30 % (292931)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2171565890:fmbsr=2:i=32576_2793 on theBenchmark for (2793ds/32576Mi)
% 0.18/29.30 % (292923)Instruction limit reached!
% 0.18/29.30 % (292923)------------------------------
% 0.18/29.30 % (292923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292923)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292923)Termination reason: Instruction limit
% 0.18/29.30 % (292923)Termination phase: Saturation
% 0.18/29.30 % (292923)Time elapsed: 6.362 s
% 0.18/29.30 % (292923)Peak memory usage: 196 MB
% 0.18/29.30 % (292923)Instructions burned: 22567 (million)
% 0.18/29.30 % (292933)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=405902665:i=11404_2775 on theBenchmark for (2775ds/11404Mi)
% 0.18/29.30 % (292927)Instruction limit reached!
% 0.18/29.30 % (292927)------------------------------
% 0.18/29.30 % (292927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292927)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292927)Termination reason: Instruction limit
% 0.18/29.30 % (292927)Termination phase: Saturation
% 0.18/29.30 % (292927)Time elapsed: 4.881 s
% 0.18/29.30 % (292927)Peak memory usage: 296 MB
% 0.18/29.30 % (292927)Instructions burned: 9158 (million)
% 0.18/29.30 % (292935)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2774677828:i=14134_2770 on theBenchmark for (2770ds/14134Mi)
% 0.18/29.30 % (292851)Instruction limit reached!
% 0.18/29.30 % (292851)------------------------------
% 0.18/29.30 % (292851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292851)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292851)Termination reason: Instruction limit
% 0.18/29.30 % (292851)Termination phase: Saturation
% 0.18/29.30 % (292851)Time elapsed: 22.056 s
% 0.18/29.30 % (292851)Peak memory usage: 205 MB
% 0.18/29.30 % (292851)Instructions burned: 88028 (million)
% 0.18/29.30 % (292937)dis+33_16_sil=32000:sac=on:random_seed=4283114832:i=15851:nm=0_2751 on theBenchmark for (2751ds/15851Mi)
% 0.18/29.30 % (292933)Instruction limit reached!
% 0.18/29.30 % (292933)------------------------------
% 0.18/29.30 % (292933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292933)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292933)Termination reason: Instruction limit
% 0.18/29.30 % (292933)Termination phase: Saturation
% 0.18/29.30 % (292933)Time elapsed: 3.449 s
% 0.18/29.30 % (292933)Peak memory usage: 199 MB
% 0.18/29.30 % (292933)Instructions burned: 11408 (million)
% 0.18/29.30 % (292939)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3008644051:avsq=on:i=17627:add=on:amm=off_2740 on theBenchmark for (2740ds/17627Mi)
% 0.18/29.30 % (292913)Instruction limit reached!
% 0.18/29.30 % (292913)------------------------------
% 0.18/29.30 % (292913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292913)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292913)Termination reason: Instruction limit
% 0.18/29.30 % (292913)Termination phase: Saturation
% 0.18/29.30 % (292913)Time elapsed: 16.348 s
% 0.18/29.30 % (292913)Peak memory usage: 942 MB
% 0.18/29.30 % (292913)Instructions burned: 29341 (million)
% 0.18/29.30 % (292941)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2511979118:s2a=on:i=53295_2730 on theBenchmark for (2730ds/53295Mi)
% 0.18/29.30 % (292929)Instruction limit reached!
% 0.18/29.30 % (292929)------------------------------
% 0.18/29.30 % (292929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292929)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292929)Termination reason: Instruction limit
% 0.18/29.30 % (292929)Termination phase: Saturation
% 0.18/29.30 % (292929)Time elapsed: 8.441 s
% 0.18/29.30 % (292929)Peak memory usage: 291 MB
% 0.18/29.30 % (292929)Instructions burned: 20139 (million)
% 0.18/29.30 % (292943)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3080371786:i=26857:ins=20_2721 on theBenchmark for (2721ds/26857Mi)
% 0.18/29.30 % (292850) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-292844-292850"...
% 0.18/29.30 % (292850)...printing done.
% 0.18/29.30 % (292850)Refutation found. Thanks to Tanya!
% 0.18/29.30 % SZS status Theorem for theBenchmark
% 0.18/29.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/29.30 % (292850)------------------------------
% 0.18/29.30 % (292850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/29.30 % (292850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.30 % (292850)CaDiCaL version: 2.1.3
% 0.18/29.30 % (292850)Termination reason: Refutation
% 0.18/29.30 % (292850)Time elapsed: 25.756 s
% 0.18/29.30 % (292850)Peak memory usage: 518 MB
% 0.18/29.30 % (292850)Instructions burned: 52647 (million)
% 0.18/29.30 % (292844)Success in time 28.879 s
% 0.18/29.30 % Vampire exiting
%------------------------------------------------------------------------------